proposition: Theorem Nat_divides_l : ∀ a b, (∃ c, a = (b * c)%nat) ↔ (b | a)%nat.
proof: Proof. intros a b. split; intros H. destruct H as (c, Hc); subst a. exists c; apply Nat.mul_comm. destruct H as (c, Hc); subst a. exists c; apply Nat.mul_comm. Qed.
imports: Utf8 QArith NPeano Sorted Psatz