proposition: Lemma addIX p1 p2 p3 p4 : addI (addI p1 p2) (addI p3 p4) = addI (addI p1 p3) (addI p2 p4).
proof: Proof. apply sig_eq => /=; by rewrite -2!mulrDl -2!addrA [in t in _+t]addrA (addrC (p2∙1) (p3∙1)) !addrA. Qed.
imports: Coq(ssreflect ssrfun ssrbool) Coq(Relation_Definitions Morphisms) Mon(SPropBase SPropMonadicStructures MonadExamples SpecificationMonads Monoid DijkstraMonadExamples) mathcomp(all_ssreflect all_algebra reals distr) Relational(Commutativity)