Definition complementary_to_neg_iff {P Q} : complementary P Q -> ¬P <-> Q. Proof. intros c. induction c as [n c]. split. - intro np. induction c as [p|q]. * contradicts p np. * exact q. - intro q. induction c as [p|_]. * intros _. exact (n p q). * intros p. exact (n p q). Defined.