proposition: Lemma axioms_opp : forall a, axioms (opp a) = axioms a.
proof: Proof. ir. apply by_cases with (axioms a); ir. assert (opp a = opp' a). uf opp. ap (Y_if H). tv. rw H0. ap iff_eq; ir. am. ap opp'_axioms. am. assert (opp a = a). uf opp. ap (Y_if_not H). tv. rww H0. Qed.
imports: Arith universe