proposition: Lemma simpl_eq_mult_l : forall a b c : nat, 0 < a -> a * b = a * c -> b = c.
proof: Proof. intros. apply le_antisym. apply simpl_le_mult_l with a. assumption. rewrite H0. apply le_n. apply simpl_le_mult_l with a. assumption. rewrite H0. apply le_n. Qed.
imports: ZArith EqNat