proposition: Lemma idealr1 : 1 \in I = false.
proof: Proof. apply: negPf; exact: proper_ideal_subproof.1. Qed.
imports: HB(structures) mathcomp(ssreflect eqtype choice ssreflect ssrbool ssrnat) mathcomp(ssrfun seq ssralg generic_quotient)