proposition: Lemma MergeLast : forall (gas : nat) (xn yn : list Q), lt (length xn + length yn) gas -> (lt 0 (length xn) \/ lt 0 (length yn)) -> ((lt 0 (length xn) /\ last (merge xn yn) 0%Q = last xn 0%Q) \/ (lt 0 (length yn) /\ last (merge xn yn) 0%Q = last yn 0%Q)).
proof: Proof. induction gas. - intros. exfalso; inversion H. - intros. destruct xn. right. split. destruct H0. exfalso; inversion H0. exact H0. destruct yn; reflexivity. destruct yn. left. split. simpl. apply le_n_S, Nat.le_0_l. simpl. reflexivity. simpl. destruct (Qle_bool q q0) eqn:des. + specialize (IHgas xn (q0 :: yn)). simpl in IHgas. destruct IHgas. simpl in H. apply le_S_n in H. exact H. right. apply le_n_S, Nat.le_0_l. * destruct H1. left. split. apply le_n_S, Nat.le_0_l. rewrite LastCons. rewrite H2. destruct xn. exfalso; inversion H1. reflexivity. rewrite MergeLength. simpl. rewrite Nat.add_succ_r. apply le_n_S, Nat.le_0_l. * destruct H1 as [_ H1]. right. split. apply le_n_S, Nat.le_0_l. rewrite <- H1. pose proof (MergeLength xn (q0 :: yn)). simpl. destruct (merge xn (q0 :: yn)). exfalso. simpl in H2. rewrite Nat.add_succ_r in H2. discriminate. reflexivity. + specialize (IHgas (q :: xn) yn). destruct IHgas. simpl in H. apply le_S_n in H. rewrite Nat.add_succ_r in H. exact H. left. apply le_n_S, Nat.le_0_l. * destruct H1 as [_ H1]. left. split. apply le_n_S, Nat.le_0_l. rewrite LastCons. simpl in H1. rewrite H1. reflexivity. pose proof (MergeLength (q :: xn) yn). simpl in H2. rewrite H2. apply le_n_S, Nat.le_0_l. * destruct H1. right. split. apply le_n_S, Nat.le_0_l. rewrite LastCons. simpl in H2. rewrite H2. destruct yn. exfalso; inversion H1. reflexivity. pose proof (MergeLength (q :: xn) yn). simpl in H3. rewrite H3. apply le_n_S, Nat.le_0_l. Qed.
imports: List Permutation Orders Sorted Mergesort QArith Qpower ConstructiveReals ConstructiveAbs ConstructiveMinMax ConstructiveSum ConstructiveLimits ConstructiveRcomplete ConstructiveDiagonal ConstructiveUniformCont