proposition: Lemma Exercise2_7B7 r: total_order r -> inductive r -> has_greatest r.
proof: Proof. move=> tor h; set F := substrate r; have si:= (@sub_refl F). move:(h F si (total_order_sub tor si)) =>[x [xa xb]]. by exists x. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)