fact: Fixpoint MergeInjectL (xn yn : list Q) (n : nat) { struct xn } : nat := let fix merge_aux yn n := match xn with | Datatypes.nil => O | Datatypes.cons x tx => match yn with | Datatypes.nil => n | Datatypes.cons y ty => if Qlt_le_dec y x then S (merge_aux ty n) else (match n with O => O | S p => S (MergeInjectL tx yn p) end) end end in merge_aux yn n.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont