proposition: Fact div_rem_uniq p n1 r1 n2 r2 : p <> 0 -> n1*p + r1 = n2*p + r2 -> r1 < p -> r2 < p -> n1 = n2 /\ r1 = r2.
proof: Proof. intros H1 H2 H3 H4. assert (n1 = n2) as E. destruct (lt_eq_lt_dec n1 n2) as [ [ H | ] | H ]; auto. + replace n2 with (n2-n1 + n1) in H2 by lia. rewrite Nat.mul_add_distr_r in H2. assert (1*p <= (n2-n1)*p) as H5. { apply Nat.mul_le_mono; lia. } simpl in H5; lia. + replace n1 with (n1-n2 + n2) in H2 by lia. rewrite Nat.mul_add_distr_r in H2. assert (1*p <= (n1-n2)*p) as H5. { apply Nat.mul_le_mono; lia. } simpl in H5; lia. + subst; lia. Qed.
imports: List Arith Lia Permutation Extraction Undecidability.Shared.Libs.DLW.Utils(utils_tac utils_list)