proposition: Lemma lem_testdep : forall e : expr Nat, match e with Var n => n >= 0 | _ => e = e end.
proof: Proof. sauto dep: on. Qed.
imports: Hammer(Tactics) Arith ZArith List Lia Hammer(Hints) Reals Lra Hammer(Reflect) Nat Psatz String Relations Sorting.Permutation