Definition pairNegation (C : ComplementaryPair) : ComplementaryPair := Part2 C,, Part1 C ,, (λ q p, pair_contradiction C p q),, coprodcomm _ _ (chooser C).
Require Import UniMath.MoreFoundations.Tactics.