proposition: Lemma encoding_algorithm_0 : forall (m n : Z) (Hm : (0 < m)%Z) (Hn : (0 < n)%Z) (H : fractionalAcc m n), m = n -> encoding_algorithm m n Hm Hn H = One.
proof: Proof. intros. apply trans_eq with (encoding_algorithm m m Hm Hm (fractionalacc0 m m (refl_equal m))). apply encoding_algorithm_equal_strong. reflexivity. symmetry in |- *. assumption. simpl in |- *; case (Z_dec' m m); [ intros [H_falsum| H_falsum] | trivial ]; Irreflex. Defined.
imports: Coq(ZArithRing) Coq(FunInd)