proposition: Theorem Nat_le_lcm_l : ∀ a b, (b ≠ 0 → a ≤ Nat.lcm a b)%nat.
proof: Proof. intros a b Hb. remember Hb as Hab; clear HeqHab. apply Nat_gcd_le_l with (b := a) in Hab. rewrite Nat.gcd_comm in Hab. unfold Nat.lcm. eapply Nat.div_le_mono in Hab. rewrite Nat.div_same in Hab. apply Nat.mul_le_mono_l with (p := a) in Hab. rewrite Nat.mul_1_r in Hab; assumption. destruct a; [ assumption | idtac ]. intros H; apply Nat.gcd_eq_0_r in H; contradiction. intros H; apply Nat.gcd_eq_0_r in H; contradiction. Qed.
imports: Utf8 QArith NPeano Sorted Psatz