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 RelationClasses Morphisms Setoid Equalities OrdersFacts GenericMinMax Bool NAxioms NMaxMin NProperties