proposition: Lemma MergeInjectRSpec : forall (gas n : nat) (xn yn : list Q), lt (length xn + length yn) gas -> lt n (length yn) -> nth (MergeInjectR xn yn n) (merge xn yn) 0%Q = nth n yn 0%Q.
proof: Proof. induction gas. - intros. exfalso; inversion H. - intros. destruct xn. + simpl. destruct yn; reflexivity. + destruct yn. exfalso; inversion H0. simpl. destruct (Qlt_le_dec q0 q). * destruct n. destruct (Qle_bool q q0) eqn:des. exfalso. pose proof (Qle_bool_iff q q0) as [H1 _]. apply (Qlt_not_le _ _ q1), H1, des. reflexivity. destruct (Qle_bool q q0) eqn:des. exfalso. pose proof (Qle_bool_iff q q0) as [H1 _]. apply (Qlt_not_le _ _ q1), H1, des. specialize (IHgas n (q :: xn) yn). simpl. simpl in IHgas. rewrite IHgas. reflexivity. clear IHgas. simpl in H. apply le_S_n in H. rewrite Nat.add_succ_r in H. exact H. simpl in H0. apply le_S_n in H0. exact H0. * destruct (Qle_bool q q0) eqn:des. simpl. rewrite IHgas. reflexivity. simpl. simpl in H. apply le_S_n in H. exact H. simpl in H0. exact H0. exfalso. pose proof (Qle_bool_iff q q0) as [_ H1]. rewrite H1 in des. discriminate. exact q1. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont