proposition: Lemma MergeInjectLSpec : forall (gas n : nat) (xn yn : list Q), lt (length xn + length yn) gas -> lt n (length xn) -> nth (MergeInjectL xn yn n) (merge xn yn) 0%Q = nth n xn 0%Q.
proof: Proof. induction gas. - intros. exfalso; inversion H. - intros. destruct xn. + simpl. destruct yn. destruct n; reflexivity. exfalso; inversion H0. + destruct yn. simpl; destruct n; reflexivity. simpl. destruct (Qlt_le_dec q0 q). * destruct (Qle_bool q q0) eqn:des. exfalso. pose proof (Qle_bool_iff q q0) as [H1 _]. apply (Qlt_not_le _ _ q1), H1, des. simpl. specialize (IHgas n (q :: xn) yn). simpl in IHgas. rewrite IHgas. reflexivity. simpl (length (q0 :: yn)) in H. rewrite Nat.add_succ_r in H. apply le_S_n in H. exact H. exact H0. * destruct n. destruct (Qle_bool q q0) eqn:des. reflexivity. exfalso. pose proof (Qle_bool_iff q q0) as [_ H1]. rewrite H1 in des. discriminate. exact q1. specialize (IHgas n xn (q0 :: yn)). 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. apply le_S_n 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