proposition: Lemma mult_O_le : forall n m : nat, m = 0%nat \/ (n <= m * n)%nat.
proof: Proof. destruct m. - now left. - right; replace n with (1 * n)%nat at 1. apply Nat.mul_le_mono_r; auto with arith. now rewrite Nat.mul_1_l. Qed.
imports: Arith Wf_nat ZArith Peano_dec ZArith_dec NatAux ZCAux ZCmisc ZSum Pmod Ppow