proposition: Theorem DistSingle_impl_Mult : DistMult_Adv _ c1 c2 A1 A2 n <= (n / 1) * (DistSingle_Adv c1 c2 B1 B2).
proof: Proof. eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. rewrite DistSingle_G1_equiv. rewrite DistSingle_G2_equiv. rewrite DistSingle_G2_equiv. rewrite DistSingle_G3_c1_equiv. rewrite DistSingle_G3_c2_equiv. eapply eqRat_refl. } eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. unfold DistSingle_G3_c1, DistSingle_G3_c2. rewrite rndNat_sumList. rewrite rndNat_sumList. rewrite sumList_factor_constant_l. rewrite sumList_factor_constant_l. rewrite ratMult_ratDistance_factor_l. eapply eqRat_refl. } eapply leRat_trans. 2:{ eapply eqRat_impl_leRat. rewrite <-ratMult_assoc. rewrite ratMult_eq_rat1. rewrite ratMult_1_l. rewrite ratDistance_comm. rewrite sumList_forNats_distance. eapply eqRat_refl. } unfold DistMult_Adv. unfold DistMult_G. rewrite ratDistance_comm. eapply eqRat_impl_leRat. eapply ratDistance_eqRat_compat. eapply evalDist_seq; intuition. comp_simp. eapply compMap_computeHybrid_0_equiv. eapply evalDist_seq; intuition. comp_simp. eapply compMap_computeHybrid_n_equiv. Unshelve. econstructor; intuition. Qed.
imports: FCF.FCF FCF.CompFold FCF.RndNat FCF.Hybrid