forall x : N, x = 0 |_| exists y : N, (x = 1 + y)%mc. Proof. refine (from_nat_stmt nat (fun s => forall x : s, x = 0 |_| exists y : s, (x = 1 + y)%mc) _). simpl. intros [|x];eauto. Qed.
Require Import Require Import Import SemiRings.