proposition: Lemma no_rht_unit_Npos1 : forall y : Npos, ~ (forall x : Npos, Npos_plus x y[=]x).
proof: Proof. intro y. case y. intros scs_elem scs_prf. cut ((1+scs_elem) <> 1). intros H. red in |- *. intros H0. apply H. unfold not in H. generalize (H0 (Build_subcsetoid_crr nat_as_CSetoid NposP 1 (S_O 0))). simpl in |- *. intuition. auto. Qed.
imports: CoRN.model.setoids.Nsetoid CoRN.model.structures.Npossec CoRN.algebra.CSetoidFun Coq(Lia)