proposition: Lemma isc_hi a b: (in_same_coset f a b) -> (inc a x /\ inc b x).
proof: Proof. move => [t [tsf p1 p2]]; rewrite (proj33 ff) in tsf. rewrite -(proj33 fpa); split; union_tac. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)