proposition: Lemma op_compatible_passes : forall (a : E) (r : E2P) (op : E2), op_within a op -> op_left_compatible a r op -> op_right_compatible a r op -> op_passes_to_quotient (quotient a r) op.
proof: Proof. ir. unfold op_passes_to_quotient in |- *; ir. unfold quotient_op in |- *. assert (inc (rep x) x). ap nonempty_rep. apply nonempty_intro with a0. am. assert (inc (rep y) y). ap nonempty_rep; apply nonempty_intro with b; au. transitivity (class_in (quotient a r) (op a0 (rep y))). apply op_right_very_compatible with y; au. assert (inc x (powerset a)). unfold quotient in H2; Ztac. assert (sub x a). ap powerset_sub. am. ap H9. am. apply op_left_very_compatible with x; au. assert (sub y a). ap powerset_sub. unfold quotient in H3; Ztac. ap H8; au. Qed.
imports: set_theory