proposition: Theorem spec_square: forall x, [square x] = [x] * [x].
proof: Proof. intros x. rewrite square_fold. destr_t x as (n,x). rewrite spec_succ_t. exact (ZnZ.spec_square_c x). Qed.
imports: Bool BigNumPrelude ZArith Lia Nnat Ndigits CyclicAxioms DoubleType Nbasic Wf_nat StreamMemo NSig NMake_gen