proposition: Lemma Decidable_complete_alt : forall P (H : Decidable P), Decidable_witness = false -> ~ P.
proof: Proof. intros. unfold not; intros. apply Decidable_spec in H1. congruence. Qed.
imports: Coq.Arith.Compare_dec Fiat.Common.Coq__8_4__8_5__Compat