proposition: Lemma H_unit_dec : forall x, H_unit x + (H_unit x -> False).
proof: Proof. intro h ; pose (np := Z_of_Z_unit Z_one) ; pose (nn := Z_of_Z_unit Z_mone). destruct (Hurwitz_dec h (mkHurwitz (2 * np) (- np) (- np) (- np))) as [e | Hnp_1]. left ; subst ; apply H_unit_1. destruct (Hurwitz_dec h (mkHurwitz (2 * nn) (- nn) (- nn) (- nn))) as [e | Hnn_1]. left ; subst ; apply H_unit_1. destruct (Hurwitz_dec h (mkHurwitz 0 np 0 0)) as [e | Hnp_i]. left ; subst ; apply H_unit_i. destruct (Hurwitz_dec h (mkHurwitz 0 nn 0 0)) as [e | Hnn_i]. left ; subst ; apply H_unit_i. destruct (Hurwitz_dec h (mkHurwitz 0 0 np 0)) as [e | Hnp_j]. left ; subst ; apply H_unit_j. destruct (Hurwitz_dec h (mkHurwitz 0 0 nn 0)) as [e | Hnn_j]. left ; subst ; apply H_unit_j. destruct (Hurwitz_dec h (mkHurwitz 0 0 0 np)) as [e | Hnp_k]. left ; subst ; apply H_unit_k. destruct (Hurwitz_dec h (mkHurwitz 0 0 0 nn)) as [e | Hnn_k]. left ; subst ; apply H_unit_k. pose (hpp := halfsub Z_one Z_one) ; pose (hpn := halfsub Z_one Z_mone) ; pose (hnp := halfsub Z_mone Z_one) ; pose (hnn := halfsub Z_mone Z_mone). destruct (Hurwitz_dec h (mkHurwitz np hpp hpp hpp)) as [e | Hh_0]. left ; subst ; apply H_unit_h. destruct (Hurwitz_dec h (mkHurwitz np hpp hpp hnp)) as [e | Hh_1]. left ; subst ; apply H_unit_h. destruct (Hurwitz_dec h (mkHurwitz np hpp hnp hpp)) as [e | Hh_2]. left ; subst ; apply H_unit_h. destruct (Hurwitz_dec h (mkHurwitz np hpp hnp hnp)) as [e | Hh_3]. left ; subst ; apply H_unit_h. destruct (Hurwitz_dec h (mkHurwitz np hnp hpp hpp)) as [e | Hh_4]. left ; subst ; apply H_unit_h. destruct (Hurwitz_dec h (mkHurwitz np hnp hpp hnp)) as [e | Hh_5]. left ; subst ; apply H_unit_h. destruct (Hurwitz_dec h (mkHurwitz np hnp hnp hpp)) as [e | Hh_6]. left ; subst ; apply H_unit_h. destruct (Hurwitz_dec h (mkHurwitz np hnp hnp hnp)) as [e | Hh_7]. left ; subst ; apply H_unit_h. destruct (Hurwitz_dec h (mkHurwitz nn hpn hpn hpn)) as [e | Hh_8]. left ; subst ; apply H_unit_h. destruct (Hurwitz_dec h (mkHurwitz nn hpn hpn hnn)) as [e | Hh_9]. left ; subst ; apply H_unit_h. destruct (Hurwitz_dec h (mkHurwitz nn hpn hnn hpn)) as [e | Hh_A]. left ; subst ; apply H_unit_h. destruct (Hurwitz_dec h (mkHurwitz nn hpn hnn hnn)) as [e | Hh_B]. left ; subst ; apply H_unit_h. destruct (Hurwitz_dec h (mkHurwitz nn hnn hpn hpn)) as [e | Hh_C]. left ; subst ; apply H_unit_h. destruct (Hurwitz_dec h (mkHurwitz nn hnn hpn hnn)) as [e | Hh_D]. left ; subst ; apply H_unit_h. destruct (Hurwitz_dec h (mkHurwitz nn hnn hnn hpn)) as [e | Hh_E]. left ; subst ; apply H_unit_h. destruct (Hurwitz_dec h (mkHurwitz nn hnn hnn hnn)) as [e | Hh_F]. left ; subst ; apply H_unit_h. right ; intros Hf ; inversion Hf. destruct u ; [apply Hnp_1 | apply Hnn_1] ; auto. destruct u ; [apply Hnp_i | apply Hnn_i] ; auto. destruct u ; [apply Hnp_j | apply Hnn_j] ; auto. destruct u ; [apply Hnp_k | apply Hnn_k] ; auto. destruct u ; destruct v ; destruct w ; destruct z ; [ apply Hh_0 | apply Hh_1 | apply Hh_2 | apply Hh_3 | apply Hh_4 | apply Hh_5 | apply Hh_6 | apply Hh_7 | apply Hh_8 | apply Hh_9 | apply Hh_A | apply Hh_B | apply Hh_C | apply Hh_D | apply Hh_E | apply Hh_F ] ; auto. Qed.
imports: ZArith Znumtheory Lia Zpow_facts MyZ Hurwitz_def