proposition: Lemma find_var_aux_lt : forall h p lvm pvm, find_var_aux h pvm lvm = Some p -> Datatypes.length lvm = (nat_of_P pvm - 1)%nat -> (nat_of_P p < nat_of_P pvm)%nat.
proof: Proof. induction lvm;simpl;try discriminate. intros pvm Heq1 Heq. assert (1 < pvm)%positive. rewrite Plt_lt;change (nat_of_P 1) with 1%nat ;lia. assert (Datatypes.length lvm = nat_of_P (Pos.pred pvm) - 1)%nat. rewrite Ppred_minus, Pminus_minus;trivial. change (nat_of_P 1) with 1%nat ;try lia. revert Heq1. destruct (Atom.reflect_eqb h a);subst. intros Heq1;inversion Heq1;clear Heq1;subst;lia. intros Heq1;apply IHlvm in Heq1;trivial. apply lt_trans with (1:= Heq1);lia. Qed.
imports: Bool List Int63 Ring63 PArray ZArith Misc State SMT_terms Euf RingMicromega ZMicromega Coq.micromega.Tauto Psatz