proposition: Lemma Exercise1_24e r r': branched r -> order r' -> branched (order_product2 r r').
proof: Proof. move=> [or bc] or'; split. apply: order_product2_or => //. move: (order_product2_sr or or') => sp. rewrite sp; move=> x xp. move: (xp) => /setX_P [px Px Qx]. move: (bc _ Px)=> [y [z [xy xz etc]]]. set s:= ((substrate r) \times (substrate r')). set y1 := J y (Q x);set z1 := J z (Q x). have y1sr: inc y1 s by rewrite /y1; apply /setX_P; split;aww;order_tac. have z1sr: inc z1 s by rewrite /s /z1; apply /setX_P; split;aww;order_tac. have leqa: gle r' (Q x) (Q x) by order_tac. exists y1; exists z1; split => //. by apply/order_product2_P;split => //; rewrite /y1; aw. by apply/order_product2_P;split => //; rewrite /z1; aw. move=> t /order_product2_P [_ _ [q1 _]] /order_product2_P [_ _ [q2 _]]. move: q1 q2; rewrite /y1/z1; aw; apply: etc. Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat)