proposition: Lemma BTreeToList_aux_concat : forall bt acc, BTreeToList_aux bt acc = BTreeToList bt ++ acc.
proof: Proof. induction bt as [| i | bt1 IHbt1 bt2 IHbt2]; [easy | easy |]. intros acc. unfold BTreeToList. simpl. rewrite IHbt2. rewrite 2IHbt1. now rewrite app_assoc. Qed.
imports: Coq(Bool Floats Reals List Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations) Specific_bigint Specific_ops Interval_helper Float_full Prog Lang_expr