proposition: Lemma rem_opp_r' a b : rem a (-b) = rem a b.
proof: Proof. destruct a, b; trivial; unfold rem; simpl; now destruct N.pos_div_eucl as (q,[|r]). Qed.
imports: BinNums BinPos Pnat BinNat Bool Equalities GenericMinMax OrdersFacts ZAxioms ZProperties DecidableClass