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