proposition: Lemma endo_compatible_passes : forall (a : E) (r : E2P) (endo : E1), endo_within a endo -> endo_compatible a r endo -> endo_passes_to_quotient (quotient a r) endo.
proof: Proof. ir. unfold endo_passes_to_quotient in |- *. set (q := quotient a r) in *. ir. assert (is_class a r x). ap in_quotient_is_class. am. assert (class_of a r (rep x) = x). ap class_of_rep. am. assert (class_of a r a0 = x). ap class_eq_class_of. am. am. set (z := Z a (fun u : E => class_in q (endo u) = quotient_endo q endo x)). assert (sub z a). unfold z in |- *; ap Z_sub. assert (sub (class_of a r (rep x)) z). ap class_of_sub. unfold z in |- *; Ztac. unfold is_class in H3. xd. unfold is_part in H3; xd. ap H3. ap nonempty_rep. am. unfold is_part in |- *; xd. ir. unfold z in |- *; Ztac. transitivity (class_in q (endo x0)). unfold q in |- *. assert (inc x0 a). ap H6; au. rewrite <- class_of_eq_class. rewrite <- class_of_eq_class. sy. ap related_classes_eq. ap H. am. ap H; am. ap H0; au. ap H. au. ap H; au. unfold z in H7; Ztac. ir. unfold z in |- *; Ztac. transitivity (class_in q (endo x0)). assert (inc x0 a). ap H6; au. unfold q in |- *. rewrite <- class_of_eq_class. rewrite <- class_of_eq_class. ap related_classes_eq. ap H; au. ap H; au. ap H0; au. ap H; au. ap H; au. unfold z in H7; Ztac. assert (inc a0 z). ap H7. rewrite H4; au. unfold z in H8; Ztac. Qed.
imports: set_theory