proposition: Lemma max_var_nformulae_mono_aux : forall l v acc, (v <= acc -> v <= fold_left F l acc)%positive.
proof: Proof. intros l; induction l as [|a l IHl] ; simpl ; [easy|]. intros. apply IHl. unfold F. apply Pos.max_case_strong;intros ; auto. eapply Pos.le_trans ; eauto. Qed.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing Coq.micromega.Tauto BinNums Zdiv Znumtheory QArith Znumtheory