proposition: Lemma imo_gleP f g: gle (increasing_mappings_order r r') f g <-> [/\ inc f (increasing_mappings r r'), inc g (increasing_mappings r r') & order_function_r (substrate r) (substrate r') r' f g].
proof: Proof. rewrite /increasing_mappings_order;split. move: imo_osr => [or''' sr0] le1. move: (arg1_sr le1) (arg2_sr le1); rewrite sr0 => sr1 sr2. by split => //; move: (iorder_gle1 le1) => /graph_on_P1 [_ _]. move=> [h1 h2 h3]; apply /(iorder_gle0P _ h1 h2) /graph_on_P1. by move: h1 h2 => /Zo_S h1 /Zo_S h2. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)