proposition: Lemma fractionalacc_1 : forall m n : Z, fractionalAcc m n -> (0 < m)%Z -> (m < n)%Z -> fractionalAcc m (n - m).
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)