proposition: Lemma sorted_trans (leT1 leT2 : rel T1) s : {in s &, (forall x y, leT1 x y -> leT2 x y)} -> sorted leT1 s -> sorted leT2 s.
proof: Proof. elim: s=> // a [] //= b l IHl leT12 /andP [leT1ab pleT1]. rewrite leT12 ?inE ?eqxx ?orbT // IHl // => x y xbcl ybcl leT1xy. by rewrite leT12 // mem_behead. Qed.
imports: mathcomp(all_ssreflect all_algebra)