fact: Fixpoint Zmod_POS (a : positive) (b : Z) : Z := match a with | xI a' => let r := Zmod_POS a' b in let r' := (2 * r + 1) in if r' <? b then r' else (r' - b) | xO a' => let r := Zmod_POS a' b in let r' := (2 * r) in if r' <? b then r' else (r' - b) | xH => if 2 <=? b then 1 else 0 end.
imports: ZArith_base Zbool ZArithRing Zcomplements Setoid Morphisms