proposition: Lemma MergeInjectLBound : forall (gas n : nat) (xn yn : list Q), lt (length xn + length yn) gas -> lt n (length xn) -> lt (MergeInjectL xn yn n) (length xn + length yn).
proof: Proof. induction gas. - intros. exfalso; inversion H. - intros. destruct xn. exfalso; inversion H0. destruct yn. simpl. rewrite Nat.add_0_r. exact H0. simpl. destruct (Qlt_le_dec q0 q). + apply le_n_S. specialize (IHgas n (q :: xn) yn). rewrite Nat.add_succ_r. apply IHgas. simpl in H. apply le_S_n in H. rewrite Nat.add_succ_r in H. exact H. exact H0. + destruct n. apply le_n_S, Nat.le_0_l. apply le_n_S. apply IHgas. simpl in H. apply le_S_n in H. exact H. simpl in H0. apply le_S_n in H0. exact H0. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont