proposition: Theorem comp_spec_impl_le : forall (A B : Set){eqda : EqDec A}{eqdb : EqDec B}(c1 : Comp A)(c2 : Comp B), forall x y, comp_spec (fun a b => a = x -> b = y) c1 c2 -> evalDist c1 x <= evalDist c2 y.
proof: Proof. intuition. despec. intuition. eapply leRat_trans. eapply eqRat_impl_leRat. eauto. eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. symmetry. eauto. } unfold marginal_l, marginal_r. dist_skip. dist_compute. exfalso. eapply n. specialize (H2 x1). intuition. eapply rat0_le_all. Qed.
imports: FCF.Crypto FCF.Bernoulli FCF.NotationV1