proposition: Lemma mult_O_le : forall n m : nat, m = 0 \/ n <= m * n.
proof: Proof. intros n m; assert (H : m=0 \/ 0 <m) by lia. destruct H. - now left. - right; replace n with (1 * n) at 1. + apply mul_le_mono_r; lia. + cbn; lia. Qed.
imports: Coq(Arith Lia)