proposition: Lemma ing_div_three : forall x, inject_Q x [/]ThreeNZ [=] inject_Q (x [/]ThreeNZ).
proof: Proof. intros. apply mult_cancel_lft with (Three:R_COrdField'). apply pos_ap_zero. apply pos_three. apply eq_symmetric_unfolded. apply eq_transitive_unfolded with (inject_Q (Three:F) [*]inject_Q (x [/]ThreeNZ)). apply mult_wdl. apply ing_nring. apply eq_transitive_unfolded with (inject_Q (Three[*]x [/]ThreeNZ)). apply eq_symmetric_unfolded. apply ing_mult. astepr (inject_Q x). apply ing_eq; algebra. Qed.
imports: CoRN.algebra.Cauchy_COF CoRN.reals.CReals