proposition: Lemma fraction_encoding_reduces : forall (a b m n : Z) (Hb : b <> 0%Z) (Hn : n <> 0%Z), (a * n)%Z = (m * b)%Z -> fraction_encoding a b Hb = fraction_encoding m n Hn.
proof: Proof. intros a b m n Hb Hn H. do 2 rewrite coding_Q. unfold spec_fraction_encoding in |- *. rewrite (Qdiv_num_denom a b n). rewrite <- Z_to_Qmult. rewrite H. rewrite Z_to_Qmult. rewrite (Qmult_sym b n). rewrite <- Qdiv_num_denom. reflexivity. replace Zero with (Z_to_Q 0); trivial; apply Z_to_Q_not_eq; assumption. replace Zero with (Z_to_Q 0); trivial; apply Z_to_Q_not_eq; assumption. Qed.
imports: Coq(FunInd) QArithSternBrocot(homographic_correctness)