proposition: Lemma Bezout_stepE a b (m n : nat) (M : 'M_(1 + m,1 + n)) (k : 'I_m) : Bezout_step a b M k = Bezout_mx a b k *m M.
proof: Proof. rewrite /Bezout_step /Bezout_mx; have [g u v a' b' _ _ _ _] := egcdrP. by rewrite combine_stepE. Qed.
imports: HB(structures) Coq(ssreflect ssrfun ssrbool Arith.Wf_nat) mathcomp(eqtype ssrnat div seq path) mathcomp(ssralg fintype perm tuple choice generic_quotient) mathcomp(matrix bigop zmodp mxalgebra poly) stronglydiscrete