proposition: Theorem spec_square : forall x, [square x] == [x] ^ 2.
proof: Proof. destruct x as [ z | n d ]. simpl; rewrite ZZ.spec_square; red; auto. simpl. destr_eqb; nzsimpl; intros. apply Qeq_refl. rewrite NN.spec_square in *; nzsimpl. rewrite Z.mul_eq_0 in *; lia. rewrite NN.spec_square in *; nzsimpl; nsubst; lia. rewrite ZZ.spec_square, NN.spec_square. red; simpl. rewrite Pos2Z.inj_mul; rewrite !Z2Pos.id; auto. apply Z.mul_pos_pos; auto. Qed.
imports: BigNumPrelude Lia QArith Qcanon Qpower Qminmax NSig ZSig QSig