proposition: Lemma list_prod_head : forall { A B : Type } (l : list A) (k : list B) (a : A) (b : B), l <> nil -> k <> nil -> nth 0 (list_prod l k) (a,b) = (nth 0 l a, nth 0 k b).
proof: Proof. intros. destruct l,k. reflexivity. contradiction. contradiction. reflexivity. Qed.
imports: QArith_base List ConstructiveReals ConstructiveRealsMorphisms ConstructiveAbs ConstructiveSum ConstructiveMinMax ConstructiveLimits ConstructivePartialFunctions CMTbase CMTIntegrableFunctions CMTIntegrableSets CMTFullSets CMTcast CMTprofile