proposition: Lemma Qhomographic_Qpositive_to_Q_equal : forall (a b c d : Z) (p : Qpositive) (H_Qhomographic_sg_denom_nonzero1 H_Qhomographic_sg_denom_nonzero2 : Qhomographic_sg_denom_nonzero c d p), Qhomographic_Qpositive_to_Q a b c d p H_Qhomographic_sg_denom_nonzero1 = Qhomographic_Qpositive_to_Q a b c d p H_Qhomographic_sg_denom_nonzero2.
proof: Proof. intros a b c d p H_Qhomographic_sg_denom_nonzero1. functional induction (Qhomographic_Qpositive_to_Q a b c d p H_Qhomographic_sg_denom_nonzero1);intros. generalize (Qhomographic_sg_denom_nonzero_nonzero_3 _ _ _ H_Qhomographic_sg_denom_nonzero1). intros [Hc| Hd]. rewrite (Qhomographic_Qpositive_to_Q_0 a b c 0 p H_Qhomographic_sg_denom_nonzero2 Hc e (refl_equal 0%Z)). apply fraction_encoding_equal. Falsum. generalize (Qhomographic_sg_denom_nonzero_nonzero_3 _ _ _ H_Qhomographic_sg_denom_nonzero1). intros [Hc| Hd]. rewrite (Qhomographic_Qpositive_to_Q_0 a b c 0 p H_Qhomographic_sg_denom_nonzero2 Hc e (refl_equal 0%Z)). apply fraction_encoding_equal. Falsum. rewrite (Qhomographic_Qpositive_to_Q_1 a b c d p H_Qhomographic_sg_denom_nonzero2 n e). apply fraction_encoding_equal. clear e0. rewrite (h_sign_equal a b c d p H_Qhomographic_sg_denom_nonzero1 H_Qhomographic_sg_denom_nonzero2) in e1. rewrite (Qhomographic_Qpositive_to_Q_2 a b c d p H_Qhomographic_sg_denom_nonzero2 n e1). reflexivity. Clear_eq_. generalize (Qhomographic_Qpositive_to_Q_homographicAcc_pos_1 a b c d p H_Qhomographic_sg_denom_nonzero1 n e1 l). assert (l1_eq_one0 := e1). rewrite (h_sign_equal a b c d p H_Qhomographic_sg_denom_nonzero1 H_Qhomographic_sg_denom_nonzero2) in l1_eq_one0. assert (z0 := l). rewrite (new_a_equal a b c d p H_Qhomographic_sg_denom_nonzero1 H_Qhomographic_sg_denom_nonzero2) in z0. rewrite (new_b_equal a b c d p H_Qhomographic_sg_denom_nonzero1 H_Qhomographic_sg_denom_nonzero2) in z0. rewrite (Qhomographic_Qpositive_to_Q_3 a b c d p H_Qhomographic_sg_denom_nonzero2 n l1_eq_one0 (Qhomographic_Qpositive_to_Q_homographicAcc_pos_1 a b c d p H_Qhomographic_sg_denom_nonzero2 n l1_eq_one0 z0) z0) . intro H_any_homographicAcc. apply f_equal with Qpositive. apply Qhomographic_Qpositive_to_Qpositive_equal_strong; [ rewrite (new_a_equal a b c d p H_Qhomographic_sg_denom_nonzero1 H_Qhomographic_sg_denom_nonzero2) | rewrite (new_b_equal a b c d p H_Qhomographic_sg_denom_nonzero1 H_Qhomographic_sg_denom_nonzero2) | rewrite (new_c_equal a b c d p H_Qhomographic_sg_denom_nonzero1 H_Qhomographic_sg_denom_nonzero2) | rewrite (new_d_equal a b c d p H_Qhomographic_sg_denom_nonzero1 H_Qhomographic_sg_denom_nonzero2) | rewrite (new_p_equal a b c d p H_Qhomographic_sg_denom_nonzero1 H_Qhomographic_sg_denom_nonzero2) ]; reflexivity. Clear_eq_. generalize (Qhomographic_Qpositive_to_Q_homographicAcc_pos_2 a b c d p H_Qhomographic_sg_denom_nonzero1 n e1 l). assert (l1_eq_one0 := e1). rewrite (h_sign_equal a b c d p H_Qhomographic_sg_denom_nonzero1 H_Qhomographic_sg_denom_nonzero2) in l1_eq_one0. assert (z0 := l). rewrite (new_a_equal a b c d p H_Qhomographic_sg_denom_nonzero1 H_Qhomographic_sg_denom_nonzero2) in z0. rewrite (new_b_equal a b c d p H_Qhomographic_sg_denom_nonzero1 H_Qhomographic_sg_denom_nonzero2) in z0. rewrite (Qhomographic_Qpositive_to_Q_4 a b c d p H_Qhomographic_sg_denom_nonzero2 n l1_eq_one0 (Qhomographic_Qpositive_to_Q_homographicAcc_pos_2 a b c d p H_Qhomographic_sg_denom_nonzero2 n l1_eq_one0 z0) z0) . intro H_any_homographicAcc. apply f_equal with Qpositive. apply Qhomographic_Qpositive_to_Qpositive_equal_strong; [ rewrite (new_a_equal a b c d p H_Qhomographic_sg_denom_nonzero1 H_Qhomographic_sg_denom_nonzero2) | rewrite (new_b_equal a b c d p H_Qhomographic_sg_denom_nonzero1 H_Qhomographic_sg_denom_nonzero2) | rewrite (new_c_equal a b c d p H_Qhomographic_sg_denom_nonzero1 H_Qhomographic_sg_denom_nonzero2) | rewrite (new_d_equal a b c d p H_Qhomographic_sg_denom_nonzero1 H_Qhomographic_sg_denom_nonzero2) | rewrite (new_p_equal a b c d p H_Qhomographic_sg_denom_nonzero1 H_Qhomographic_sg_denom_nonzero2) ]; reflexivity. Clear_eq_. generalize (Qhomographic_Qpositive_to_Q_homographicAcc_neg_1 a b c d p H_Qhomographic_sg_denom_nonzero1 n e0 l). assert (l1_eq__minus_one0 := e0). rewrite (h_sign_equal a b c d p H_Qhomographic_sg_denom_nonzero1 H_Qhomographic_sg_denom_nonzero2) in l1_eq__minus_one0. assert (z0 := l). rewrite (new_a_equal a b c d p H_Qhomographic_sg_denom_nonzero1 H_Qhomographic_sg_denom_nonzero2) in z0. rewrite (new_b_equal a b c d p H_Qhomographic_sg_denom_nonzero1 H_Qhomographic_sg_denom_nonzero2) in z0. rewrite (Qhomographic_Qpositive_to_Q_5 a b c d p H_Qhomographic_sg_denom_nonzero2 n l1_eq__minus_one0 (Qhomographic_Qpositive_to_Q_homographicAcc_neg_1 a b c d p H_Qhomographic_sg_denom_nonzero2 n l1_eq__minus_one0 z0) z0) . intro H_any_homographicAcc. apply f_equal with Qpositive. apply Qhomographic_Qpositive_to_Qpositive_equal_strong; [ rewrite (new_a_equal a b c d p H_Qhomographic_sg_denom_nonzero1 H_Qhomographic_sg_denom_nonzero2) | rewrite (new_b_equal a b c d p H_Qhomographic_sg_denom_nonzero1 H_Qhomographic_sg_denom_nonzero2) | rewrite (new_c_equal a b c d p H_Qhomographic_sg_denom_nonzero1 H_Qhomographic_sg_denom_nonzero2) | rewrite (new_d_equal a b c d p H_Qhomographic_sg_denom_nonzero1 H_Qhomographic_sg_denom_nonzero2) | rewrite (new_p_equal a b c d p H_Qhomographic_sg_denom_nonzero1 H_Qhomographic_sg_denom_nonzero2) ]; reflexivity. Clear_eq_. generalize (Qhomographic_Qpositive_to_Q_homographicAcc_neg_2 a b c d p H_Qhomographic_sg_denom_nonzero1 n e0 l). assert (l1_eq__minus_one0 := e0). rewrite (h_sign_equal a b c d p H_Qhomographic_sg_denom_nonzero1 H_Qhomographic_sg_denom_nonzero2) in l1_eq__minus_one0. assert (z0:=l). rewrite (new_a_equal a b c d p H_Qhomographic_sg_denom_nonzero1 H_Qhomographic_sg_denom_nonzero2) in z0. rewrite (new_b_equal a b c d p H_Qhomographic_sg_denom_nonzero1 H_Qhomographic_sg_denom_nonzero2) in z0. rewrite (Qhomographic_Qpositive_to_Q_6 a b c d p H_Qhomographic_sg_denom_nonzero2 n l1_eq__minus_one0 (Qhomographic_Qpositive_to_Q_homographicAcc_neg_2 a b c d p H_Qhomographic_sg_denom_nonzero2 n l1_eq__minus_one0 z0) z0) . intro H_any_homographicAcc. apply f_equal with Qpositive. apply Qhomographic_Qpositive_to_Qpositive_equal_strong; [ rewrite (new_a_equal a b c d p H_Qhomographic_sg_denom_nonzero1 H_Qhomographic_sg_denom_nonzero2) | rewrite (new_b_equal a b c d p H_Qhomographic_sg_denom_nonzero1 H_Qhomographic_sg_denom_nonzero2) | rewrite (new_c_equal a b c d p H_Qhomographic_sg_denom_nonzero1 H_Qhomographic_sg_denom_nonzero2) | rewrite (new_d_equal a b c d p H_Qhomographic_sg_denom_nonzero1 H_Qhomographic_sg_denom_nonzero2) | rewrite (new_p_equal a b c d p H_Qhomographic_sg_denom_nonzero1 H_Qhomographic_sg_denom_nonzero2) ]; reflexivity. Defined.
imports: Coq(FunInd)