Definition stnprod_step { n : nat } ( f : ⟦S n⟧ -> nat ) : stnprod f = stnprod (f ∘ dni lastelement) * f lastelement. Proof. intros. apply idpath. Defined.
Require Import UniMath.MoreFoundations.Tactics. Require Import UniMath.MoreFoundations.DecidablePropositions. Require Import UniMath.MoreFoundations.NegativePropositions.