proposition: Lemma less_wdr : forall x y z : F, x [<] y -> y [=] z -> x [<] z.
proof: Proof. Proof Ccsr_wdr F cof_less. Lemma less_wdl : forall x y z : F, x [<] y -> x [=] z -> z [<] y. Proof Ccsr_wdl F cof_less. End COrdField_axioms. Declare Left Step less_wdl. Declare Right Step less_wdr. Section OrdField_basics. Variable R : COrdField. Lemma less_imp_ap : forall x y : R, x [<] y -> x [#] y. Proof. intros x y H. elim (less_conf_ap _ x y); intros. apply b. left. auto. Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)