proposition: Lemma set0_width: the_order_width emptyset = \0c /\ the_order_length emptyset = \0c.
proof: Proof. have aux x: inc x (\Po substrate emptyset) -> cardinal x <=c \0c. rewrite (proj2 set0_osr); move/setP_P /sub_set0 ->. rewrite cardinal_set0;fprops. split. apply:(the_max_card_on_set_prop2 NS0);split. exists emptyset; last exact: cardinal_set0. by apply/free_subsetsP; split ; [fprops|move => x y /in_set0]. by move => x /Zo_S /aux. apply:(the_max_card_on_set_prop2 NS0);split. exists emptyset; last exact: cardinal_set0. apply: empty_total_suborders. by move => x /Zo_S/aux. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)