proposition: Lemma term_gt_incl_succ : term_gt << IR_succ.
proof: Proof. intros l r lr v. destruct (mint_eval_equiv l r v). simpl in * . unfold succ, Rof, I, succ_vec. symmetry in H. symmetry in H0. rewrite (vec_ge_mor H H0), (Vforall2_elim_nth dim_pos H), (Vforall2_elim_nth dim_pos H0). change (succ_vec (mint_eval v (mi_of_term (ABterm.inject_term (Nat.le_max_l (maxvar l) (maxvar r))))) (mint_eval v (mi_of_term (ABterm.inject_term (Nat.le_max_r (maxvar l) (maxvar r)))))). apply mint_eval_mon_succ. hyp. Qed.
imports: Coq(Setoid) CoLoR(LogicUtil Matrix OrdSemiRing VecUtil AMonAlg SN RelUtil AWFMInterpretation NatUtil AMatrixBasedInt)