proposition: Theorem DistMult_impl_RepeatCore : RepeatCore_Adv P c1 c2 A1 A2 <= DistMult_Adv _ c1 c2 A1 DM_RC_B2 n + expRat k1 n + expRat k2 n.
proof: Proof. unfold RepeatCore_Adv, DistMult_Adv. repeat rewrite DM_RC_G1_equiv. repeat rewrite DM_RC_G2_equiv. eapply leRat_trans. eapply ratDistance_le_trans. eapply DM_RC_G2_G3_close; intuition. eauto. rewrite ratDistance_comm. eapply ratDistance_le_trans. eapply DM_RC_G2_G3_close; intuition. eauto. repeat rewrite DM_RC_G4_equiv. repeat rewrite DM_RC_G5_equiv. repeat rewrite DM_RC_G6_equiv. repeat rewrite DistMult_G_equiv. eapply leRat_refl. rewrite <- ratAdd_assoc. rewrite ratAdd_comm. rewrite <- ratAdd_assoc. rewrite ratDistance_comm. intuition. intuition. intuition. intuition. intuition. Qed.
imports: FCF.FCF FCF.CompFold FCF.RndNat FCF.Hybrid