proposition: Lemma fractionsimplified : forall f : F, simplified (fraction f).
proof: Proof. simple induction f ; simpl. - split ; auto. - intro f0; case (fraction f0). inversion_clear 1;split; auto. - intro f0; case (fraction f0). inversion_clear 1; split; auto. Qed.
imports: ZArith