proposition: Lemma square_spec n : square n = n * n.
proof: Proof. destruct n; trivial; simpl; f_equal; apply Pos.square_spec. Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass