proposition: Lemma mult_le_l : forall a b c : nat, b <= c -> a * b <= a * c.
proof: Proof. simple induction a; simpl in |- *; [ auto with arith | intros ]. apply plus_le_compat; auto with arith. Qed.
imports: Arith Constants Le_lt_compl