proposition: Lemma RList_P11 : forall l1 l2:list R, length (cons_ORlist l1 l2) = (length l1 + length l2)%nat.
proof: Proof. induction l1 as [ | r r0 H]; [ intro; reflexivity | intros; simpl; rewrite (H (insert l2 r)); rewrite RList_P10; apply INR_eq; rewrite S_INR; do 2 rewrite plus_INR; rewrite S_INR; ring ]. Qed.
imports: List Rbase Rfunctions