proposition: Lemma homographicAcc_wf : forall (a b c d : Z) (p : Qpositive), (0 < a + b)%Z -> (0 < c + d)%Z -> (0 <= a)%Z -> (0 <= b)%Z -> (0 <= c)%Z -> (0 <= d)%Z -> homographicAcc a b c d p.
proof: Proof. intros a b c d p Hab Hcd Ha Hb Hc Hd. set (ha := Build_Z_pos a Ha) in *. set (hb := Build_Z_pos b Hb) in *. set (hc := Build_Z_pos c Hc) in *. set (hd := Build_Z_pos d Hd) in *. generalize Hab Hcd Ha Hb Hc Hd. change ((0 < ha + hb)%Z -> (0 < hc + hd)%Z -> (0 <= ha)%Z -> (0 <= hb)%Z -> (0 <= hc)%Z -> (0 <= hd)%Z -> homographicAcc ha hb hc hd p) in |- *. apply qlt_wf_rec_without_zeros_and_One with (P := fun (r s t u : Z) (p1 : Qpositive) => (0 < r + s)%Z -> (0 < t + u)%Z -> (0 <= r)%Z -> (0 <= s)%Z -> (0 <= t)%Z -> (0 <= u)%Z -> homographicAcc r s t u p1). intros a0 b0 c0 d0 p0 hyp1_aux. assert (hyp1 : forall (r s t u : Z) (p1 : Qpositive), qlt r s t u p1 a0 b0 c0 d0 p0 -> (0 < r + s)%Z -> (0 < t + u)%Z -> (0 <= r)%Z -> (0 <= s)%Z -> (0 <= t)%Z -> (0 <= u)%Z -> homographicAcc r s t u p1). intros. change (homographicAcc (Build_Z_pos r H2) (Build_Z_pos s H3) (Build_Z_pos t H4) (Build_Z_pos u H5) p1) in |- *. apply hyp1_aux; repeat assumption. destruct p0 as [q| q| ]. case (top_more_informative a0 b0 c0 d0). intros. apply homographicacc1. discriminate. assumption. apply hyp1. right. split. reflexivity. apply top_more_5. assumption. apply top_more_1. assumption. assumption. apply Zle_minus. apply (top_more_4 _ _ _ _ t). apply Zle_minus. apply (top_more_4' _ _ _ _ t). assumption. assumption. intro. case (top_more_informative c0 d0 a0 b0). intros. apply homographicacc2. discriminate. assumption. assumption. apply hyp1. right. split. reflexivity. apply top_more_5'. assumption. assumption. apply top_more_1. assumption. assumption. assumption. apply Zle_minus. apply (top_more_4 _ _ _ _ t). apply Zle_minus. apply (top_more_4' _ _ _ _ t). intros. apply homographicacc3. assumption. assumption. apply hyp1. left. unfold bin_lt in |- *. apply compare_nR. replace 0%Z with (0 + 0)%Z. apply Zplus_le_lt_compat. assumption. assumption. constructor. replace 0%Z with (0 + 0)%Z. apply Zplus_le_lt_compat. assumption. assumption. constructor. assumption. apply Zlt_le_weak. assumption. assumption. apply Zlt_le_weak. assumption. case (top_more_informative a0 b0 c0 d0). intros. apply homographicacc1. discriminate. assumption. apply hyp1. right. split. reflexivity. apply top_more_5. assumption. apply top_more_1. assumption. assumption. apply Zle_minus. apply (top_more_4 _ _ _ _ t). apply Zle_minus. apply (top_more_4' _ _ _ _ t). assumption. assumption. intro. case (top_more_informative c0 d0 a0 b0). intros. apply homographicacc2. discriminate. assumption. assumption. apply hyp1. right. split. reflexivity. apply top_more_5'. assumption. assumption. apply top_more_1. assumption. assumption. assumption. apply Zle_minus. apply (top_more_4 _ _ _ _ t). apply Zle_minus. apply (top_more_4' _ _ _ _ t). intros. apply homographicacc3'. assumption. assumption. apply hyp1. left. unfold bin_lt in |- *. apply compare_dL. replace 0%Z with (0 + 0)%Z. apply Zplus_lt_le_compat. assumption. assumption. constructor. replace 0%Z with (0 + 0)%Z. apply Zplus_lt_le_compat. assumption. assumption. constructor. apply Zlt_le_weak. assumption. assumption. apply Zlt_le_weak. assumption. assumption. intros. apply homographicacc0. reflexivity. assumption. assumption. Defined.
imports: QArithSternBrocot(Merge_Order) Coq(Wf_nat)