proposition: Lemma RList_P1 : forall (l:list R) (a:R), ordered_Rlist l -> ordered_Rlist (insert l a).
proof: Proof. intros; induction l as [| r l Hrecl]. - simpl; unfold ordered_Rlist; intros; simpl in H0; elim (Nat.nlt_0_r _ H0). - simpl; case (Rle_dec r a); intro. + assert (H1 : ordered_Rlist l). * unfold ordered_Rlist; unfold ordered_Rlist in H; intros; assert (H1 : (S i < pred (length (r :: l)))%nat); [ simpl; replace (length l) with (S (pred (length l))); [ apply -> Nat.succ_lt_mono; assumption | apply Nat.lt_succ_pred with 0%nat; apply Nat.neq_0_lt_0; red; intro; rewrite H1 in H0; simpl in H0; elim (Nat.nlt_0_r _ H0) ] | apply (H _ H1) ]. * assert (H2 := Hrecl H1); unfold ordered_Rlist; intros; induction i as [| i Hreci]. -- simpl; assert (H3 := RList_P0 l a); elim H3; intro. ++ rewrite H4; assumption. ++ induction l as [| r1 l Hrecl0]; [ simpl; assumption | rewrite H4; apply (H 0%nat); simpl; apply Nat.lt_0_succ ]. -- simpl; apply H2; simpl in H0; apply Nat.succ_lt_mono; replace (S (pred (length (insert l a)))) with (length (insert l a)); [ assumption | symmetry; apply Nat.lt_succ_pred with 0%nat; apply Nat.neq_0_lt_0; red; intro; rewrite H3 in H0; elim (Nat.nlt_0_r _ H0) ]. + unfold ordered_Rlist; intros; induction i as [| i Hreci]; [ simpl; auto with real | change (pos_Rl (r :: l) i <= pos_Rl (r :: l) (S i)); apply H; simpl in H0; simpl; apply (proj2 (Nat.succ_lt_mono _ _) H0) ]. Qed.
imports: List Rbase Rfunctions