proposition: Lemma combine_stepE (a b c d : R) (m n : nat) (M : 'M_(1 + m,1 + n)) (k : 'I_m) : combine_step a b c d M k = combine_mx a b c d k *m M.
proof: Proof. apply/matrixP=> i j; have [g u v a' b' _ _ _ _] := egcdrP a b. rewrite !mxE (bigD1 ord0) // !mxE (bigD1 (lift 0 k)) // !mxE /=. case H: (i == 0). rewrite big1=> [|l /andP [/negbTE H1 /negbTE H2]]. by rewrite (eqP H) !eqxx !mulr1n !mxE !mulr0 !addr0 mulr0n add0r mulr1. by rewrite !mxE (eqP H) (eq_sym 0 l) H1 H2 mulr0n !mulr0 !add0r mul0r. case H': (i == lift 0 k). rewrite big1=> [|l /andP [/negbTE H1 /negbTE H2]]. by rewrite (eqP H') !(eqxx,mulr1n,mxE,mulr0,addr0,mulr1,mulr0n,add0r). by rewrite !mxE (eqP H') !(eq_sym _ l) eqxx H1 H2 mulr0n !mulr0 !add0r mul0r. rewrite (bigD1 i); last by rewrite H H'. rewrite !mxE big1=> [/=|l /andP [/andP [/negbTE H1 /negbTE H2] /negbTE H3]]. by rewrite H H' eqxx !(mulr0n,mulr0,mulr1n,addr0,mul0r,add0r,mul1r). by rewrite !mxE H H' H1 H2 (eq_sym i l) H3 mulr0n !mulr0 !addr0 mul0r. 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