proposition: Lemma pow_twice_r a b : a^(2*b) == a^b * a^b.
proof: Proof. rewrite two_succ. nzsimpl. destruct (le_gt_cases 0 b). - now rewrite pow_add_r. - rewrite !pow_neg_r. + now nzsimpl. + trivial. + now apply add_neg_neg. Qed.
imports: Bool ZAxioms ZMulOrder ZParity ZSgnAbs NZPow