proposition: Lemma MergeLength : forall (xn yn : list Q), length (merge xn yn) = plus (length xn) (length yn).
proof: Proof. intros. pose proof (Permuted_merge xn yn). apply Permutation_length in H. rewrite <- H. apply app_length. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont