proposition: Lemma three_integers_dec_inf : forall a b c : Z, {a = 0%Z /\ b = 0%Z /\ c = 0%Z} + {~ (a = 0%Z /\ b = 0%Z /\ c = 0%Z)}.
proof: Proof. intros. case (Z_zerop a). intro. case (Z_zerop b). intro. case (Z_zerop c); [ intro; left; repeat split; assumption | intro; right; intros (H, (H1, H2)); Falsum ]. intro; right; intros (H, (H1, H2)); Falsum. intro; right; intros (H, (H1, H2)); Falsum. Defined.
imports: Coq(ZArithRing) QArithSternBrocot(Qhomographic_sign) QArithSternBrocot(Zaux)