proposition: Lemma help_with_choice {A B C : Type} {D E : A -> B -> Prop} {P : A -> B -> C -> Prop} : (forall (a : A) (b : B), D a b -> E a b-> exists c : C, P a b c) -> (exists f : forall (a : A) (b : B), D a b -> E a b -> C, forall (a : A) (b : B) (d : D a b) (e : E a b), P a b (f a b d e)).
proof: Proof. intro H. apply (dep_choice _ _ (fun a f => forall (b : B) (d : D a b) (e : E a b), P a b (f b d e))). intro a. apply (dep_choice _ _ (fun b f => forall (d : D a b) (e : E a b), P a b (f d e))). intro b. apply (choice (fun d f => forall (e : E a b), P a b (f e))). intro d. apply (choice (fun e c => P a b c)). apply (H a b d). Qed.
imports: Lia Arith Arith.Compare ClassicalChoice ChoiceFacts Libs.Analysis.SubsequencesMetric