proposition: Lemma egcd_recP : forall n a b, norm b <= n -> let e := (egcd_rec a b n) in gcdr a b %= e.1 * a + e.2 * b.
proof: Proof. elim=> [|n ihn] a b /=. by rewrite leqn0 => /eqP/norm_eq0->; rewrite mul1r mul0r addr0 gcdr0. move=> nbSn. case b0: (b == 0)=> /=; first by rewrite (eqP b0) mul1r mulr0 addr0 gcdr0. have := (ihn b (a %% b) _). case: (egcd_rec _ _)=> u v=> /= ihn' /=. rewrite (eqd_trans (gcdrE _ _)) ?(eqd_trans (ihn' _ _)) //; do ?by rewrite -ltnS (leq_trans (mod_spec _ _)) ?b0 //. rewrite mulrBl addrA [v * a + _]addrC -mulrA -addrA -mulrBr /div b0. case: edivP ihn'=> /= q r. move/eqP; rewrite addrC -subr_eq; move/eqP=>->. by rewrite b0 /= => nrb; apply; rewrite -ltnS (leq_trans nrb). 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