proposition: Lemma Qpairio_eq k n l m: natp k -> natp n -> natp l -> natp m -> (Qpairi k n) = (Qpairi l m) -> (k = l /\ n = m).
proof: Proof. move=> kN nN lN mN eq1. move: Qpairio_osr => [qo qs]. have mqs: inc (Qpairi k n) (substrate Qpairi_o). rewrite qs; apply /Qpairis_prP; exists k; exists n;split => //. have aux: gle Qpairi_o (Qpairi k n) (Qpairi k n) by order_tac. move: (aux); rewrite {2} eq1 => /(Qpairio_gle2P kN nN lN mN). move => [p [pN np le1 le2]]. move: aux; rewrite {1} eq1 => /(Qpairio_gle2P lN mN kN nN). move => [q [qN nq le3 le4]]. move: (Nsum_M0le p nN)(Nsum_M0le q mN). rewrite -np -nq => le5 le6. have nm: n = m by exact: cleA. have r1: n +c \0c = n +c p by rewrite csum0r; [rewrite -np nm | fprops]. have r2: m +c \0c = m +c q by rewrite csum0r; [rewrite -nq nm | fprops]. move: le1; rewrite -(csum_eq2l nN NS0 pN r1). rewrite cpowx0 cprod1r; fprops => kl. move: le3; rewrite -(csum_eq2l mN NS0 qN r2). rewrite cpowx0 cprod1r; fprops => lk. split => //; exact: cleA. Qed.
imports: mathcomp(ssreflect ssrbool eqtype ssrfun)