proposition: Lemma less_cotransitive_unfolded : forall x y : R, x [<] y -> forall z, x [<] z or z [<] y.
proof: Proof. Proof less_cotransitive. Lemma pos_ap_zero : forall x : R, [0] [<] x -> x [#] [0]. Proof. intros x H. apply Greater_imp_ap. assumption. Defined.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)