proposition: Lemma the_greatest_interval r a b: order r -> gle r a b -> the_greatest (induced_order r (interval_cc r a b)) = b.
proof: Proof. move=> or ab. have sab: (sub (interval_cc r a b) (substrate r)) by apply: Zo_S. have asr: inc b (substrate r) by apply: (arg2_sr ab). have aicc: inc b (interval_cc r a b). by apply: Zo_i =>//; split=>//; order_tac. have [or' sr]:= (iorder_osr or sab). apply: the_greatest_pr2; [exact | hnf;rewrite sr]. split =>//;move=> x xi; apply/iorder_gle0P => //. by move/Zo_P: xi => [_ []]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)