proposition: Lemma max_var_nformulae_mono_aux' : forall l acc acc', (acc <= acc' -> fold_left F l acc <= 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_le_compat_r; auto. Qed.
imports: List Bool OrderedRing RingMicromega ZCoeff Refl ZArith_base ZArithRing Ztac EnvRing Coq.micromega.Tauto BinNums Zdiv Znumtheory QArith Znumtheory