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