Buenas,
Estuve intentando sacar una demostración de la identidad de Bezout, y me salió sin usar el algoritmo de Euclides (parecido a como se demuestra Bezout para enteros en Discreta 2). Me quedo alguna duda sobre como formalizar la ultima parte, sobre todo la consecuencia del final donde entiendo que hay que considerar una constante en la clausura algebraica del cuerpo.
Dejo la demo por si a alguien le interesa :)