proposition: Lemma bounded_pexpr_le : forall p p', (nat_of_P p <= nat_of_P p')%nat -> forall pe, bounded_pexpr p pe -> bounded_pexpr p' pe.
proof: Proof. unfold is_true;induction pe;simpl;trivial. rewrite <- !Zlt_is_lt_bool; rewrite <- Ple_le in H. intros H1;apply Z.lt_le_trans with (1:= H1);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. Qed.
imports: Bool List Int63 Ring63 PArray ZArith Misc State SMT_terms Euf RingMicromega ZMicromega Coq.micromega.Tauto Psatz