proposition: Lemma class_of_in_quotient : forall (a : E) (r : E2P) (x : E), inc x a -> inc (class_of a r x) (quotient a r).
proof: Proof. ir. unfold quotient in |- *; ap Z_inc. ap powerset_inc. ap class_of_sub; au. ap lem1. ap class_of_class; au. Qed.
imports: set_theory