proposition: Lemma negpaths0sx (x : nat) : ¬ (0 = S x).
proof: Proof. set (f := λ n : nat, match n with O => true | S m => false end). apply (negf (@maponpaths _ _ f 0 (S x)) nopathstruetofalse). Defined.
imports: UniMath.Foundations.Sets