proposition: Lemma forall_disjoint_pairs_equiv : forall { X : Type } (l : list X) (P : X -> X -> Prop) (x : X), (forall i j : nat, lt i j -> lt j (length l) -> P (nth i l x) (nth j l x)) -> forall_disjoint_pairs l P.
proof: Proof. induction l. - intros. constructor. - intros. split. + apply (IHl P x). intros. apply (H (S i) (S j)). apply le_n_S, H0. apply le_n_S, H1. + clear IHl. apply Forall_forall. intros. apply (In_nth _ _ a) in H0. destruct H0 as [n [H0 H1]]. subst x0. specialize (H O (S n)). simpl in H. rewrite (nth_indep _ a x). apply H. apply le_n_S, Nat.le_0_l. apply le_n_S, H0. exact H0. Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile