proposition: Lemma sqrtrem_spec p : SqrtSpec (sqrtrem p) p.
proof: Proof. revert p. fix sqrtrem_spec 1. intro p; destruct p as [p|p|]; try destruct p; try (constructor; easy); apply sqrtrem_step_spec; auto. Qed.
imports: BinNums Eqdep_dec EqdepFacts RelationClasses Morphisms Setoid Equalities Orders OrdersFacts GenericMinMax PeanoNat BinPosDef