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