proposition: Lemma eq_ler : forall x y, (x == y) = (x <<= y) && (y <<= x) .
proof: Proof. Proof . move=> x y; apply/idP/idP . + by move/eqP => ->; rewrite ler_refl . + by case/andP=> Hxy Hyx; rewrite (ler_antisym Hxy Hyx) . Qed . Lemma ltr_lerne : forall x y, (x <<! y) = (x <<= y) && (x != y) . Proof . move=> x y; rewrite ler_ltreq; case e: (x <<! y); rewrite /= ?andbN //. by case exy: (x == y) e => //; rewrite (eqP exy) ltr_irrefl. Qed . Lemma ltr_ne : forall x y, (x <<! y) -> (x != y) . Proof. by move=> x y; rewrite ltr_lerne; case/andP. Qed.
imports: mathcomp(ssreflect eqtype ssrbool ssrnat fintype seq ssrfun) mathcomp(bigop choice)