proposition: Lemma rem_opp_l' 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