proposition: Lemma ltr_ler_trans : forall x y z, x <<! y -> y <<= z -> x <<! z .
proof: Proof. Proof . move=> x y z Hxy Hyz; rewrite ltr_lerne; apply/andP; split . + by apply ler_trans with y; first apply ltrW . + apply/eqP; move=> H; subst z . rewrite ltr_lerne in Hxy; case/andP: Hxy => Hxy . by rewrite eq_ler Hyz Hxy . Qed . Lemma ler_ltr_trans : forall x y z, x <<= y -> y <<! z -> x <<! z. Proof. move=> x y z Hxy Hyz; rewrite ltr_lerne; apply/andP; split . + by apply ler_trans with y; last apply ltrW . + apply/eqP; move=> H; subst z . rewrite ltr_lerne in Hyz; case/andP: Hyz => Hyz . by rewrite eq_ler Hyz Hxy . Qed.
imports: mathcomp(ssreflect eqtype ssrbool ssrnat fintype seq ssrfun) mathcomp(bigop choice)