proposition: Lemma nth_list_prod : forall {A B : Type} (l:list A) (k:list B) (a:A) (b:B) (n:nat), lt n (length l * length k) -> nth n (list_prod l k) (a,b) = (nth (n / length k) l a, nth (n mod (length k)) k b).
proof: Proof. induction l. - intros. exfalso; inversion H. - intros. destruct (le_lt_dec (length k) n). + assert (n - length k < length l * length k)%nat. { rewrite (Nat.add_lt_mono_r _ _ (length k)), Nat.sub_add. 2: exact l0. rewrite Nat.add_comm. exact H. } specialize (IHl k a0 b (n - length k)%nat H0). clear H. simpl (list_prod (a :: l) k). rewrite app_nth2. 2: rewrite map_length; exact l0. rewrite map_length. rewrite IHl. pose proof (Nat.le_exists_sub (length k) n l0) as [i [H _]]. subst n. rewrite Nat.add_sub. apply f_equal2. replace ((i + length k) / length k)%nat with (S (i / length k))%nat. reflexivity. replace (i + length k)%nat with (i + 1*length k)%nat. rewrite Nat.div_add. rewrite Nat.add_comm. reflexivity. 2: rewrite Nat.mul_1_l; reflexivity. intro abs. rewrite Nat.add_sub, abs, Nat.mul_0_r in H0. inversion H0. replace (i + length k)%nat with (i + 1*length k)%nat. rewrite Nat.mod_add. reflexivity. intro abs. rewrite Nat.add_sub, abs, Nat.mul_0_r in H0. inversion H0. rewrite Nat.mul_1_l. reflexivity. + clear IHl. simpl (list_prod (a :: l) k). rewrite app_nth1. 2: rewrite map_length; exact l0. rewrite Nat.div_small, Nat.mod_small. 2: exact l0. 2: exact l0. simpl. rewrite (nth_indep _ (a0,b) (a,b)). rewrite map_nth. reflexivity. rewrite map_length. exact l0. Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile