proposition: Lemma empty_total_suborders r: inc emptyset (total_suborders r).
proof: Proof. apply/total_subordersP; split; [ fprops |]. have ->: (induced_order r emptyset) = emptyset. by apply/set0_P => t /setI2_P [_] /setX_P [_ /in_set0]. exact: (worder_total(proj1 set0_wor)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)