proposition: Lemma ltR_max z : max x y < z <-> x < z /\ y < z.
proof: Proof. case: (max x y) / IFR_cases => _ [[leyx]|[ltxy]] ->. by split=> [ltxz | []//]; split=> //; apply: leR_lt_trans leyx ltxz. by split=> [ltyz | []//]; split=> //; apply: ltR_trans ltxy ltyz. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div order) mathcomp(ssralg ssrnum ssrint rat intdiv) Coq(Morphisms Setoid) fourcolor(real realsyntax)