proposition: Lemma square_spec p : square p = p * p.
proof: Proof. induction p as [p IHp|p IHp|]. - rewrite square_xI. simpl. now rewrite IHp. - rewrite square_xO. simpl. now rewrite IHp. - trivial. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef