proposition: Theorem Single_impl_ListHybrid : ListHybrid_Advantage <= maxA / 1 * maxDistance.
proof: Proof. rewrite Single_impl_ListHybrid_sum. eapply leRat_trans. eapply sumList_le. intros. eapply maxDistance_correct. rewrite sumList_body_const. rewrite forNats_length. rewrite ratMult_comm. intuition. Qed.
imports: FCF.FCF FCF.CompFold