proposition: Lemma one_less_four : ([1]:R) [<] Four.
proof: Proof. apply less_leEq_trans with (Three:R). exact one_less_three. apply less_leEq; exact three_less_four. Qed.
imports: CoRN.tactics.FieldReflection CoRN.tactics.Rational CoRN.algebra.CSetoids Coq(Lia)