proposition: Lemma square_xO p : p~0 * p~0 = (p*p)~0~0.
proof: Proof. simpl. now rewrite mul_comm. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef