proposition: Lemma par_mergerest_decomp : forall Al bl P l, CPropToProp (par_mergerest Al bl P) l <-> CPropToProp (par_mergerest Al bl CTrue) l /\ CPropToProp P l.
proof: Proof. induction Al; [easy |]. intros [| [|] bl] P l; simpl; [| apply IHAl |]. - rewrite merge_decomp. rewrite (merge_decomp _ (CAnd _ _) _). now simpl. - rewrite IHAl. rewrite (IHAl _ (CAnd _ _) _). now simpl. 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