proposition: Lemma ProdIntegrableSubsetsDisjoint : forall {A : Set} (hn : list (A -> Prop)) (l l0 : list bool) (x : A), length l = length l0 -> length l = length hn -> l <> l0 -> ~ (SubsetIntersectFilter hn (SubsetUnion hn) l x /\ SubsetIntersectFilter hn (SubsetUnion hn) l0 x).
proof: Proof. intros. simpl. intros [H2 H3]. pose proof (SubsetsDifferent l l0 H H1) as [n [nlen ndiff]]. pose proof (DomainProdSubsetIntersect hn (SubsetUnion hn) l x n H2). pose proof (DomainProdSubsetIntersect hn (SubsetUnion hn) l0 x n H3). destruct (nth_error hn n) eqn:des. destruct (nth_error l n) eqn:desl. destruct (nth_error l0 n) eqn:des0. destruct b. destruct b0. exact (ndiff eq_refl). contradiction. destruct b0. contradiction. exact (ndiff eq_refl). rewrite nth_error_None, <- H in des0. exact (proj1 (Nat.lt_nge _ _) nlen des0). rewrite nth_error_None in desl. exact (proj1 (Nat.lt_nge _ _) nlen desl). rewrite nth_error_None, <- H0 in des. exact (proj1 (Nat.lt_nge _ _) nlen des). Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile