proposition: Lemma simpl_le_mult_l : forall a b c : nat, 0 < a -> a * b <= a * c -> b <= c.
proof: Proof. simple induction a. intros. elim (lt_n_O 0). assumption. intros a1 IH. intros. simpl in H0. elim (le_or_lt b c). intro. assumption. intro. elim (lt_not_le (S a1 * c) (S a1 * b)). apply lt_mult_l. assumption. assumption. Qed.
imports: ZArith EqNat