proposition: Theorem Kdiv_inv_eq_0: forall x y, x/y = 0 -> y<>0 -> x = 0.
proof: Proof. intros x y H1 H2. apply trans_equal with (y * (x/y)); try field; auto. rewrite H1; ring. Qed.
imports: Arith_base Field_tac Ring Eqdep_dec FGroup List UList ZArith