proposition: Lemma item_addr0_mulr : forall n x, @iter R n (+%R x) 0 = x *~ n.
proof: Proof. intros n x. induction n as [| n ih]. - cbn. reflexivity. - simpl. rewrite ih. unfold intmul. rewrite GRing.mulrS. reflexivity. Qed.
imports: Mon(FiniteProbabilities SPropMonadicStructures SpecificationMonads MonadExamples SPropBase) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples Commutativity GenericRulesSimple) mathcomp(all_ssreflect all_algebra reals distr realsum) Crypt(Axioms ChoiceAsOrd SubDistr Couplings Theta_dens Theta_exCP LaxComp FreeProbProg UniformDistrLemmas Prelude choice_type StateTransformingLaxMorph RulesStateProb)