proposition: Lemma bounded_bformula_le : forall p p', (nat_of_P p <= nat_of_P p')%nat -> forall (bf:BFormula (Formula Z) isProp), bounded_bformula p bf -> bounded_bformula p' bf.
proof: Proof. unfold is_true;induction bf;simpl;trivial. - destruct a;unfold bounded_formula;simpl. rewrite andb_true_iff;intros (H1, H2). rewrite (bounded_pexpr_le _ _ H _ H1), (bounded_pexpr_le _ _ H _ H2);trivial. - rewrite !andb_true_iff;intros (H1, H2);auto. - rewrite !andb_true_iff;intros (H1, H2);auto. - rewrite !andb_true_iff;intros (H1, H2);auto. - rewrite !andb_true_iff;intros (H1, H2);auto. - rewrite !andb_true_iff;intros (H1, H2);auto. Qed.
imports: Bool List Int63 Ring63 PArray ZArith Misc State SMT_terms Euf RingMicromega ZMicromega Coq.micromega.Tauto Psatz