proposition: Lemma constant_increasing1: nonempty E -> forall y y', inc y F -> inc y' F -> (gle r' y y' <-> gle (increasing_mappings_order r r') (constant_function E F y) (constant_function E F y')).
proof: Proof. move=> [u usr] y y' ysr ysr'. split; last by move => h; move: (imo_incr or' h usr); rewrite !constant_V. move:(constant_increasing ysr)(constant_increasing ysr') => pa pb. move:(constant_prop E ysr)(constant_prop E ysr') => pc pd. move=> yy'; apply /imo_gleP => //;split => //; split => //. by move => i isr; rewrite ! constant_V. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)