proposition: Lemma fractionalacc_2 : forall m n : Z, fractionalAcc m n -> (0 < n)%Z -> (n < m)%Z -> fractionalAcc (m - n) n.
proof: Proof. simple destruct 1; intros; trivial; Falsum; apply (Z.lt_irrefl n0); [ rewrite H0 in H2 | apply Z.lt_trans with m0 ]; assumption. Defined.
imports: Coq(ZArithRing) Coq(FunInd)