proposition: Lemma sup_monotone a b c: inc a E -> gle r b c-> gle r (sup r a b) (sup r a c).
proof: Proof. move=> asr bc. move: (lattice_sup_pr lr asr (arg1_sr bc)). move: (lattice_sup_pr lr asr (arg2_sr bc)). move: lr => [or _] [p1 p2 _][_ _ p6]. by apply: p6; [ apply: p1 | apply: order_transitivity p2]. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)