proposition: Theorem prime37 : is_prime 37.
proof: Proof. unfold is_prime; intros. check_lt_not_divides. Time Qed. End primes. Ltac clear_all := match goal with | id:_ |- _ => clear id; clear_all | |- _ => idtac end. Theorem clear_example_thm : forall (x y z:nat), x<z->z=2*x->0<x->x=2*y->y<z->x>y. Proof. intros x y z H H1 H2 H3. generalize H1 H2 H3; clear_all; intros; lia. Qed.
imports: ZArith List Arith Lia Reals Lra