proposition: Fact FRACTAN_cases ll : { Exists (fun c => fst c = 0) ll } + { Forall (fun c => snd c <> 0) ll } + { p : nat & { mm | Forall (fun c => fst c <> 0) ll /\ Exists (fun c => snd c = 0) ll /\ ll = (p,0):: mm /\ p <> 0 } } + { p : nat & { q : nat & { mm | Forall (fun c => fst c <> 0) ll /\ Exists (fun c => snd c = 0) ll /\ ll = (p,q):: mm /\ q <> 0 /\ p <> 0 } } }.
proof: Proof. destruct (Forall_Exists_dec (fun c : nat * nat => snd c <> 0)) with (l := ll) as [ ? | Hl1 ]; auto. { intros (p, q); destruct (eq_nat_dec q 0); simpl; subst; [ right | left]; lia. } assert (Exists (fun c => snd c = 0) ll) as H1. { revert Hl1; induction 1; [ constructor 1 | constructor 2 ]; auto; lia. } clear Hl1. destruct (Forall_Exists_dec (fun c : nat * nat => fst c <> 0)) with (l := ll) as [ Hl3 | Hl3 ]. { intros (p, q); destruct (eq_nat_dec p 0); simpl; subst; [ right | left ]; lia. } 2: { do 3 left; clear H1; revert Hl3; induction 1; [ constructor 1 | constructor 2 ]; auto; lia. } case_eq ll. { intro; subst; exfalso; inversion H1. } intros (p,q) mm Hll. destruct (eq_nat_dec p 0) as [ Hp | Hp ]. { subst; rewrite Forall_cons_inv in Hl3; simpl in Hl3; lia. } destruct q. + left; right; exists p, mm; subst; auto. + right; exists p, (S q), mm; subst; repeat (split; auto). Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils_tac utils_list utils_nat gcd rel_iter pos vec)