proposition: Lemma Ndiv_non_0 : forall a b, (a | b) -> 1 <= b -> 1 <= a.
proof: Proof. intros. destruct a. destruct H. rewrite Nat.mul_0_r in H. rewrite H in H0. exact H0. auto with arith. Qed.
imports: Coq(Arith Euclid Compare Lia)