proposition: Lemma SubsetsDifferent : forall (h k : list bool), length h = length k -> h <> k -> { n : nat | lt n (length h) /\ nth_error h n <> nth_error k n }.
proof: Proof. induction h. - intros. exfalso. destruct k. exact (H0 eq_refl). inversion H. - intros. destruct k. exfalso; inversion H. simpl in H. inversion H. clear H. destruct a, b. + destruct (IHh k H2) as [n [nlen ndiff]]. intro abs. subst k. exact (H0 eq_refl). exists (S n). split. apply le_n_S, nlen. exact ndiff. + exists O. split. apply le_n_S, Nat.le_0_l. simpl. discriminate. + exists O. split. apply le_n_S, Nat.le_0_l. simpl. discriminate. + destruct (IHh k H2) as [n [nlen ndiff]]. intro abs. subst k. exact (H0 eq_refl). exists (S n). split. apply le_n_S, nlen. exact ndiff. Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile