proposition: Lemma lem_gcd_step : forall a b d, b <> 0 -> is_gcd d b (a mod b) -> is_gcd d a b.
proof: Proof. unfold is_gcd, is_cd. intros a b d Hb. sintuition. - destruct (Nat.eq_dec d 0) as [Hd|Hd]. + subst; reflexivity. + assert (Hc1: exists c1, b = d * c1). { strivial use: Nat.mod_divides. } assert (Hc2: exists c2, a mod b = d * c2). { strivial use: Nat.mod_divides. } assert (Hc3: exists c3, a = b * c3 + a mod b). { srun eauto use: Nat.div_mod. } clear -Hc1 Hc2 Hc3 Hd. destruct Hc1 as [c1 H1]. destruct Hc2 as [c2 H2]. destruct Hc3 as [c3 H3]. subst. rewrite H2 in H3. subst. assert (H: d * c1 * c3 + d * c2 = (c1 * c3 + c2) * d) by lia. rewrite H. auto using Nat.mod_mul. - enough ((a mod b) mod d' = 0) by auto. destruct (Nat.eq_dec d' 0) as [Hd|Hd]. + subst; reflexivity. + assert (Hc1: exists c1, b = d' * c1) by hauto use: Nat.mod_divides. assert (Hc2: exists c2, a = d' * c2) by hauto use: Nat.mod_divides. assert (Hc3: exists c3, a = b * c3 + a mod b). { exists (a / b); auto using Nat.div_mod. } clear -Hc1 Hc2 Hc3 Hd Hb. destruct Hc1 as [c1 H1]. destruct Hc2 as [c2 H2]. destruct Hc3 as [c3 H3]. subst. clear - Hb Hd. rewrite Nat.mul_mod_distr_l; [| lia | lia ]. rewrite Nat.mul_comm. apply Nat.mod_mul; assumption. Qed.
imports: Hammer(Tactics) Hammer(Hammer) Program Arith Lia