proposition: Theorem constant_cost_compose_binary_const_l : forall (A B C D: Type) (b : B)(f2 : A -> C)(f3 : B -> C -> D) c1 c2, cost f2 c1 -> cost (f3 b) c2 -> cost (fun a => f3 b (f2 a)) (c1 + c2).
proof: Proof. intuition. eapply constant_cost_le. eapply (constant_cost_compose f2 (fun _ x => f3 b x)). eauto. eapply constant_cost_const. intuition. eauto. lia. Qed.
imports: FCF.Crypto