proposition: Theorem Nat_gcd_le_l : ∀ a b, (a ≠ 0 → Nat.gcd a b ≤ a)%nat.
proof: Proof. intros a b Ha. pose proof (Nat.gcd_divide_l a b) as Hg. destruct Hg as (c, Hg). rewrite Hg in |- * at 2. unfold Nat.gcd. destruct c; [ contradiction | simpl ]. apply le_plus_l. Qed.
imports: Utf8 QArith NPeano Sorted Psatz