proposition: Lemma isc_rel1P a b: inc a x -> inc b x -> ((in_same_coset f a b) <-> (cover_at (graph f) a = cover_at (graph f) b)).
proof: Proof. move => ax bx; split. move => [t [tsf pa pb]]. rewrite (proj33 ff) in tsf. by rewrite(cover_at_pr fpa tsf pa) (cover_at_pr fpa tsf pb). move => h. move: (cover_at_in fpa ax) (cover_at_in fpa bx); rewrite -h - (proj33 ff). set s := (cover_at (graph f) a); move => [pa pb] [pc pd]. by exists s. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)