proposition: Lemma ltr_sorderb : sorderb (@ltbDef G) .
proof: Proof. Proof . by case G => [T [? []]] . Qed . Lemma ltr_irrefl : irreflexive (@ltbDef G). Proof . by case ltr_sorderb . Qed . Lemma ltr_trans : transitive (@ltbDef G) . Proof . by case ltr_sorderb . Qed . Lemma ltr_lcompat : lcompatible (@ltbDef G) . Proof . by case G => [T [? []]] . Qed . Lemma ltr_rcompat : rcompatible (@ltbDef G). Proof. by move=> x y z; rewrite mulrC [z * _]mulrC; exact: ltr_lcompat. Qed.
imports: mathcomp(ssreflect eqtype ssrbool ssrnat fintype seq ssrfun) mathcomp(bigop choice)