proposition: Lemma ZFap_symmetric : forall n : Z, Csymmetric (ZFap n).
proof: Proof. intro n. unfold Csymmetric in |- *. unfold ZFap in |- *. intros x y. case x. case y. intuition. Qed.
imports: Coq.ZArith.ZArith CoRN.algebra.CSetoids