proposition: Lemma Uint63_canonic : forall x y, to_Z x = to_Z y -> x = y.
proof: Proof. Proof to_Z_inj. Lemma ring_theory_switch_eq : forall A (R R':A->A->Prop) zero one add mul sub opp, (forall x y : A, R x y -> R' x y) -> ring_theory zero one add mul sub opp R -> ring_theory zero one add mul sub opp R'. Proof. intros A R R' zero one add mul sub opp Impl Ring. constructor; intros; apply Impl; apply Ring. Qed.
imports: Cyclic63 CyclicAxioms