proposition: Lemma order_total_extension r: order r -> exists r', [/\ total_order r', substrate r' = substrate r & sub r r'].
proof: Proof. move=> or. set (E:= substrate r). move: (fo_osr E) => [or1 sr1]. have rr: (inc r (substrate (finer_order E))) by rewrite sr1; apply /ordersP. move: (inductive_max_greater or1 (@fo_inductive E) rr) => [m]. move/ Exercise2_1bP => [tm sm] /fo_gleP [_ _ _ _ rm]. by exists m. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)