proposition: Theorem expnat_plus : forall k1 k2 n, expnat n (k1 + k2) = expnat n k1 * expnat n k2.
proof: Proof. induction k1; simpl in *; intuition. rewrite IHk1. rewrite Nat.mul_assoc. trivial. Qed.
imports: Arith micromega.Lia Coq.NArith.BinNat