proposition: Theorem lia_fail1 : 0 = 1.
proof: Proof. Fail lia. Abort. Theorem lia_fail2 : forall (n : nat), n >= 1 -> 2 ^ n = 2 * 2 ^ (n - 1). Proof. Fail lia. Abort. Require Import Ring. Theorem mult_comm : forall (n m : nat), n * m = m * n. Proof. intros n m. ring. Qed.
imports: Coq(Arith List) LF(IndProp) Coq(Lia)