proposition: Lemma gcd_mod : forall a b r, (a mod b)%P = Npos r -> gcd a b = gcd b r.
proof: Proof. intros a b r H;unfold gcd. assert (log2 r <= log2 (xO r)). simpl;zsimpl;lia. assert (H1 := mod_lt _ _ _ H). pattern (gcd_log2 b r (xO r)) at 1; rewrite gcd_log2_Zle_log;auto with zarith. destruct (Z_lt_le_dec a b) as [z|z]. pattern (gcd_log2 a b (xO b)) at 1; rewrite gcd_log2_xO_Zlt;trivial. rewrite (lt_mod _ _ z) in H;inversion H. assert (r <= b). lia. generalize (gcd_log2_None _ _ H2). destruct (gcd_log2 b r r);intros;trivial. assert (log2 b <= log2 (xO b)). simpl;zsimpl;lia. pattern (gcd_log2 a b (xO b)) at 1; rewrite gcd_log2_Zle_log;auto with zarith. pattern (gcd_log2 a b b) at 1;rewrite (gcd_log2_mod _ _ z _ H). assert (r <= b). lia. generalize (gcd_log2_None _ _ H3). destruct (gcd_log2 b r r);intros;trivial. Qed.
imports: ZArith Lia ZCmisc Zwf