proposition: Lemma prod_plus n m u : prod (n + m) u = prod n u * prod m (shift n u).
proof: Proof. revert u; induction n; intros u; simpl. - ring_simplify. apply prod_ext; compute; auto. - rewrite IHn. ring_simplify. f_equal. apply prod_ext; intros; unfold shift. f_equal; auto with *. Qed.
imports: Lia Reals Psatz