proposition: Lemma total_order_width r: total_order r -> nonempty (substrate r) -> the_order_width r = \1c.
proof: Proof. move => tor [u usr]. apply:(the_max_card_on_set_prop2 NS1);split. exists (singleton u); first by apply:(Exercise1_5b (proj1 tor) usr). by rewrite cardinal_set1. by move => x / (Exercise1_5e tor) /cardinal_small_set. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)