proposition: Lemma Exercise2_7A3: [/\ order_on NNstar (canonical_du2 Nat Nat) & (forall x x', gle NNstar x x' <-> [/\ inc x (canonical_du2 Nat Nat), inc x' (canonical_du2 Nat Nat) & [\/ [/\ Q x = C0, Q x' = C0 & (P x) <=c (P x')], [/\ Q x <> C0, Q x' <> C0 & (P x') <=c (P x)] | (Q x = C0 /\ Q x' <> C0)]])].
proof: Proof. rewrite /NNstar. move: Nat_order_wor=> [[or _] s1]. move: (opp_osr or) => [or1]; rewrite s1 => s2. split; first split. by apply: orsum2_or. by rewrite orsum2_sr // s1 s2. move=> x x'; split. move /orsum2_gleP; rewrite s1 s2; move => [p1 p2 p3];split => //. case: p3; first by move => [q1 q2] /Nat_order_leP [_ _ s4]; constructor 1. by move => [q1 q2] /opp_gleP /Nat_order_leP [_ _ s4]; constructor 2. by move => q1; constructor 3. move => [p1 p2 p3]; apply /orsum2_gleP; rewrite s1 s2; split => //. have aux: forall z, inc z (canonical_du2 Nat Nat) -> inc (P z) Nat. by move=> z /candu2P[_ ]; case; case. case: p3. move => [q1 q2 q3]; constructor 1;split => //;apply /Nat_order_leP. by split => //; apply: aux. move => [q1 q2 q3]; constructor 2;split => //. by apply /opp_gleP/Nat_order_leP;split => //; apply: aux. by move => q1; constructor 3. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)