fact: Fixpoint reassoc (exp : ppT1) (fuel :nat) : ppT1 := match exp, fuel with | exp, 0 => exp | PP_add e (PP_add f g), S n => reassoc (PP_add (PP_add (reassoc e n) (reassoc f n)) (reassoc g n)) n | PP_add e f , S n => PP_add (reassoc e n) (reassoc f n) | PP_mult e i , S n=> PP_mult (reassoc e n) i | PP_exp e f , S n => PP_exp (reassoc e n) (reassoc f n) | e, _=> e end.
imports: Coq(Arith Max Bool Lia Compare_dec Relations Ensembles Wellfounded Bool RelationClasses Operators_Properties ArithRing Logic.Eqdep_dec) hydras(More_Arith Restriction DecPreOrder) hydras(OrdNotations)