proposition: Lemma less_cotransitive : cotransitive (cof_less (c:=R)).
proof: Proof. red in |- *. intros x y H z. generalize (less_imp_ap _ _ H); intro H0. elim (ap_cotransitive_unfolded _ _ _ H0 z); intro H1. elim (ap_imp_less _ _ H1). auto. intro H2. right. apply (less_transitive_unfolded _ _ _ _ H2 H). elim (ap_imp_less _ _ H1). auto. intro H2. left. apply (less_transitive_unfolded _ _ _ _ H H2). Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)