proposition: Theorem elim_example : forall n:nat, n <= 1 -> n*n <= 1.
proof: Proof. intros n H. destruct (sqr_01 n); auto. inversion_clear H; auto. inversion_clear H0; auto. Qed.
imports: ZArith List Arith Lia Zwf Relations JMeq List Vector