proposition: Theorem sqr_mult2 : forall n : nat, sqr (n * n) = n.
proof: Proof. intros n; apply sqr_inv; auto with arith. apply Nat.le_lt_trans with (S n * n); auto with arith. simpl in |- *; auto with arith. Qed.
imports: Coq(Arith ArithRing)