proposition: Theorem spec_even_aux: forall x, if even x then [x] mod 2 = 0 else [x] mod 2 = 1.
proof: Proof. intros x. rewrite even_fold. destr_t x as (n,x). exact (ZnZ.spec_is_even x). Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen