proposition: Lemma diagonal_width r: order r -> finite_set (substrate r) -> (order_width r (cardinal (substrate r)) <-> r = diagonal (substrate r)).
proof: Proof. move => or fse. split => hyp; last first. split. exists (substrate r) => //; apply /free_subsetsP; split => //. by rewrite hyp => a b asr bsr /diagonal_pi_P []. by move => x /free_subsetsP [] /sub_smaller. set_extens t; last by move/diagonal_i_P => [{4} <- ps <-]; order_tac. move => tr; apply /diagonal_i_P. move: (proj41 or _ tr) (pr1_sr tr) (pr2_sr tr) => pt Ps Qs. split => //. have cp: (gle r (P t) (Q t)) by move:tr; rewrite - {1} pt. move: (proj1 hyp) => [X /free_subsetsP [Xsr Xfree] cX]. have XX := (cardinal_setC5 fse Xsr cX). rewrite - XX in Ps Qs. exact: (Xfree (P t) (Q t) Ps Qs cp). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)