proposition: Lemma gcd_spec1 a b: 0 <> b -> gcd a b = gcd (Nat.modulo a b) b.
proof: Proof. funelim (gcd a b); intros. rewrite Nat.Div0.mod_0_l; auto. simp gcd. simpl in H. rewrite (Nat.mod_small (S n) (S n0)); auto. set(x := S n) in *. set (y := S n0) in *. rewrite gcd_equation_3. rewrite Heq. simpl. reflexivity. rewrite refl. rewrite Nat.Div0.mod_same; auto. rewrite H; auto. rewrite mod_minus; auto. Qed.
imports: Equations(Equations) Relations Arith Lia ExtrOcamlBasic