proposition: Lemma CArithExprToTree_Psucc : forall t, CArithExprToTree (Psucc t) = exprsucc (CArithExprToTree t).
proof: Proof. induction t as [| | | OP | | | | |]; simpl; intros. 5, 6, 7, 9: now rewrite IHt. 1, 2, 3, 5: easy. now destruct OP; rewrite IHt1; rewrite IHt2. 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