proposition: Lemma exp2_Plus : forall n p, exp2 (n + p) = (exp2 n * exp2 p)%positive.
proof: Proof. induction n; cbn. - reflexivity. - intro p; now rewrite IHn. Qed.
imports: Coq(Relations RelationClasses Lia List) Param(Param) additions(More_on_positive)