proposition: Lemma Rdiv_eq_0_inv : forall a b, a / b = 0 -> b <> 0 -> a = 0.
proof: Proof. intros a b Hab Hb ; destruct (Rmult_integral _ _ Hab) as [Ha | Hb']. apply Ha. assert (Hb'' : / b <> 0) by (apply Rinv_neq_0_compat ; assumption). apply False_ind, Hb'', Hb'. Qed.
imports: RIneq MyNeq Rfunctions Lra