proposition: Lemma set0_width_2 r: order r -> order_width r \0c -> substrate r = emptyset.
proof: Proof. move => or [_ ha]; case:(emptyset_dichot (substrate r)) => // - [x xsr]. case: (cleNgt(ha _ (Exercise1_5b or xsr))). rewrite cardinal_set1; exact: clt_01. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)