proposition: Lemma ing_min : forall x : F, inject_Q [--]x [=] [--] (inject_Q x).
proof: Proof. intros. unfold inject_Q in |- *. simpl in |- *; intro H. elim H; intro. elim a; intros N HN. elim HN; clear H a HN; intros e He HN; simpl in HN. apply (less_irreflexive_unfolded _ e). apply leEq_less_trans with ([0]:F); auto. astepr ( [--]x[-][--]x); eauto with arith. elim b; intros N HN. elim HN; clear H b HN; intros e He HN; simpl in HN. apply (less_irreflexive_unfolded _ e). apply leEq_less_trans with ([0]:F); auto. astepr ( [--]x[-][--]x); eauto with arith. Qed.
imports: CoRN.algebra.Cauchy_COF CoRN.reals.CReals