proposition: Lemma comb : forall (p: Prop) (x: Z), p -> (p -> x = 0) -> x = 0.
proof: Proof. intros. Fail lia. Abort. Lemma comb2 : forall (p: Prop) (x: Z), p -> (p -> x = 0) -> x = 0. Proof. intros. intuition lia. Qed.
imports: Cdcl.Itauto Uint63 Bool ZArith Lia