Lemma negProp_to_complementary P : ∏ (Q : negProp P), P ⨿ Q <-> complementary P Q. Proof. intros [Q [i [r s]]]; simpl in *. split. * intros pq. split. - intros p q. apply s. + assumption. + assumption. - assumption. * intros [j c]. assumption. Defined.