proposition: Lemma eq_subset_pr2 a b a' b': a =c a' -> b =c b' -> a <=s b -> a' <=s b'.
proof: Proof. move=> /card_eqP /EqS [g [[injg _] sg tg]] /card_eqP [f [[injf _] sf tf]]. move => [h [ih sh th]]; exists ((f \co h) \co g); split => //; aw; trivial. have ch: f \coP h by split => // ;try fct_tac; ue. apply: compose_fi => //. apply: compose_fi => //. by split => //; try fct_tac; aw; ue. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)