proposition: Lemma mult_lt_O_compat : forall a b, lt O a -> lt O b -> lt O (mult a b).
proof: Proof. intros a b Ha Hb. destruct a; [ inversion Ha | clear Ha ]. destruct b; [ inversion Hb | clear Hb ]. simpl. apply Nat.lt_0_succ. Qed.
imports: ZArith Reals Lia Lra DiscrR Rfunctions