proposition: Lemma exp_sum x y z: T1nf x -> T1nf y -> z ^(x+y) = z ^x * z ^y.
proof: Proof. move => nx ny; rewrite /T1exp. move: (nf_rev_sum nx ny); case: eqP; move => h [-> ->]. by rewrite h expO_n0 T1mul1n - mulA expF_add. by rewrite -mulA (mulA (exp_F z _)) exp_FO ? mulA ? expO_add //; apply/eqP. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat) mathcomp(fintype bigop)