proposition: Lemma identity_increasing_decreasing x (r := diagonal x) : (increasing_fun (identity x) r r /\ decreasing_fun (identity x) r r).
proof: Proof. have [oi si]:= (diagonal_osr x). move:(identity_prop (substrate r)); rewrite {1} si => pa. split;split => // a b rab; rewrite !idV //;try (rewrite - si; order_tac). by move/diagonal_pi_P: rab => [ax <-]; apply/diagonal_pi_P. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)