fact: Definition plus (e1 e2 : aexpr) := match e1, e2 with | Nval n1, Nval n2 => Nval (n1 + n2) | Nval 0, _ => e2 | _, Nval 0 => e1 | _, _ => Aplus e1 e2 end.
imports: Hammer(Tactics) Arith ZArith List Lia Hammer(Hints) Reals Lra Hammer(Reflect) Nat Psatz String