proposition: Theorem radix_val_inj : forall r1 r2, radix_val r1 = radix_val r2 -> r1 = r2.
proof: Proof. intros (r1, H1) (r2, H2) H. simpl in H. revert H1. rewrite H. intros H1. apply f_equal. apply eqbool_irrelevance. Qed.
imports: Coq(ZArith Lia Zquot)