proposition: Lemma TriangleInequality : ∀ {Game_export : Interface} {F G H : Game_Type Game_export} {ϵ1 ϵ2 ϵ3}, F ≈[ ϵ1 ] G → G ≈[ ϵ2 ] H → F ≈[ ϵ3 ] H → ∀ LA A, ValidPackage LA Game_export A_export A → fdisjoint LA F.(locs) → fdisjoint LA G.(locs) → fdisjoint LA H.(locs) → ϵ3 A <= ϵ1 A + ϵ2 A.
proof: Proof. intros Game_export F G H ε₁ ε₂ ε₃ h1 h2 h3 LA A vA hF hG hH. unfold adv_equiv in *. erewrite <- h1, <- h2, <- h3 by eassumption. apply ler_dist_add. Qed.
imports: Coq(Utf8) Relational(OrderEnrichedCategory OrderEnrichedRelativeMonadExamples) mathcomp(ssrnat ssreflect ssrfun ssrbool ssrnum eqtype choice reals distr seq all_algebra fintype realsum) extructures(ord fset fmap) Mon(SPropBase) Crypt(Prelude Axioms ChoiceAsOrd SubDistr Couplings RulesStateProb UniformStateProb UniformDistrLemmas StateTransfThetaDens StateTransformingLaxMorph choice_type pkg_core_definition pkg_notation pkg_tactics pkg_composition pkg_heap pkg_semantics pkg_lookup) Equations.Prop.DepElim Equations(Equations) Crypt(FreeProbProg)