proposition: Lemma AtomToGoal_correct : forall i a l, compatible_atom a = true -> Interval.contains (Iaux.convert i) (Xreal.Xreal (Tree.eval (CArithExprToTree (getCArithExpr a)) l)) -> IH.R.eval_goal_bnd prec (AtomToGoal a) i = true -> AtomToProp a l.
proof: Proof. intros i a l Ha Hcont Heg. generalize IH.R.eval_goal_bnd_correct. intros H. specialize (H prec (AtomToGoal a) i (Tree.eval (CArithExprToTree (getCArithExpr a)) l) Hcont Heg). clear Hcont Heg. destruct a; simpl in *; [| | | unfold Rrnd.maxval;rewrite minus_IZR | | | | easy..]; apply (compatible_correct _ l) in Ha; now rewrite <-Ha. 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