proposition: Lemma gcd_0_l : forall d : nat, d > 0 -> gcd 0 (Z_of_nat d) d.
proof: Proof. unfold gcd in |- *. unfold common_div in |- *. split. split. split with 0. simpl in |- *. rewrite <- mult_n_O. reflexivity. split with 1. simpl in |- *. rewrite <- mult_n_Sm. rewrite <- mult_n_O. simpl in |- *. rewrite abs_inj. reflexivity. intros. apply div_le. assumption. elim H0. intros. rewrite abs_inj in H2. assumption. Qed.
imports: ZArith Wf_nat lemmas natZ divides modulo