fact: Example silly_presburger_example : forall m n o p, m + n <= n + o /\ o + 3 = p + 3 -> m <= p.
imports: Coq(Bool.Bool) Coq(Init.Nat) Coq(Arith.Arith) Coq(Arith.EqNat) Coq(Lia) Coq(Lists.List) Coq(Strings.String) LF(Maps)