proposition: Lemma op_right_very_compatible : forall (a : E) (r : E2P) (op : E2), op_within a op -> op_right_compatible a r op -> forall x b c d : E, inc x (quotient a r) -> inc b a -> inc c x -> inc d x -> class_in (quotient a r) (op b c) = class_in (quotient a r) (op b d).
proof: Proof. ir. set (f := fun u : E => op b u). assert (endo_within a f). unfold endo_within in |- *. ir. unfold f in |- *. ap H; au. assert (endo_compatible a r f). unfold endo_compatible in |- *. ir. unfold f in |- *. ap H0; au. pose (endo_compatible_passes H5 H6). unfold endo_passes_to_quotient in (type of e). unfold f in (type of e). transitivity (quotient_endo (quotient a r) (fun u : E => op b u) x). ap e; au. sy. ap e; au. Qed.
imports: set_theory