forall (x y : N), x + y = 0 -> x = 0 /\ y = 0. Proof. refine (from_nat_stmt nat (fun s => forall x y : s, x + y = 0 -> x = 0 /\ y = 0) _). simpl. apply plus_eq_zero. Qed.
Require Import Require Import Import SemiRings.