proposition: Lemma OT_opposite_sum r f: order r -> substrate r = domain f -> order_type_fam f -> OT_opposite (OT_sum r f) = OT_sum (opp_order r) (Lg (substrate r) (fun z => OT_opposite (Vg f z))).
proof: Proof. move=> or sr alo. rewrite /OT_opposite /OT_sum Lgd; apply: order_type_unique. set s1 := order_sum _ _. have alor : forall x , inc x (domain f) -> order (Vg f x). move=> i idf; apply: (OT_prop2 (alo _ idf)). set s2:= order_sum r (Lg (domain f) (fun z => (Vg f z))). apply: (@orderIT (opp_order s2)). apply: OT_opposite1;apply: (@orderIT s1). apply: OT_prop0. apply: orsum_or;split => //; hnf; aw; trivial => i idf; rewrite LgV//. apply: (OT_prop3 (alor _ idf)). rewrite /s1 /s2. apply: orsum_invariant2 ; aww. rewrite sr;move=> i isr; rewrite !LgV//; apply: (OT_prop0 (alor _ isr)). set g := (Lg (domain f) (fun z => (opp_order (Vg f z)))). move: (opp_osr or) => [pa pb]. have ta: orsum_ax (opp_order r) g. rewrite /g;split => //;fprops;aw;first by ue. hnf; aw;move=> i idf; rewrite LgV//; exact: (proj1 (opp_osr (alor _ idf))). have os2: order s2. by apply: orsum_or; split => //; hnf; aw; trivial; move=> i idf; rewrite LgV//; apply: alor. have tb:orsum_ax r (Lg (domain f) (fun z => Vg f z)). split => //; hnf; aw; trivial. move=> i idf; rewrite LgV//; move: (alor _ idf) => aux; fprops. have osg: order (order_sum (opp_order r) g) by apply: orsum_or. have ss:substrate (order_sum (opp_order r) g) = substrate s2. rewrite /s2 orsum_sr // orsum_sr //. rewrite /sum_of_substrates /fam_of_substrates /g; aw. apply: f_equal; apply: Lg_exten => // x xdf; rewrite !LgV //. apply (proj2 (opp_osr (alor _ xdf))). apply: (@orderIT (order_sum (opp_order r) g)). move: ( identity_fb (substrate s2)) => hh. move: (opp_osr os2) => [oo3 sr2]. exists (identity (substrate s2)). split;fprops; first split;aww. hnf;aw;move => x y xsr ysr; rewrite !idV //. have qy:inc (Q y) (domain f). move: ysr; rewrite /s2 orsum_sr // => h. by move: (du_index_pr1 h) => [h1 _]; move: h1; aw. have qx:inc (Q x) (domain f). move: xsr; rewrite /s2 orsum_sr // => h. by move: (du_index_pr1 h) => [h1 _]; move: h1; aw. have sgs2: sum_of_substrates g = substrate s2. by move: ss; rewrite /s2 orsum_sr // orsum_sr //. have sgs3: (sum_of_substrates (Lg (domain f) (Vg f))) = substrate s2. rewrite /s2 orsum_sr //. split. move /opp_gleP => ha; apply /orsum_gleP; rewrite sgs2;split => //. move: ha => /orsum_gleP [pa' pb']; case => pc. by left; apply /opp_gltP. rewrite /order_sum_r;right; move: pc => [];rewrite LgV//; move => -> pc; split => //. by rewrite /g ! LgV//; apply /opp_gleP. move /orsum_gleP => [_ _ h]; apply /opp_gleP; apply /orsum_gleP. rewrite sgs3;split => //; case: h; first by move /opp_gltP => h;left. move => [sq]; rewrite /g LgV//;move /opp_gleP => h. right; rewrite !LgV//. split => //; ue. apply: orsum_invariant2 => //; rewrite /g pb; aw; trivial. rewrite sr;move=> i isr; rewrite !LgV//. move: (alor _ isr) => aux. have aux2: order (opp_order (Vg f i)) by apply: (proj1 (opp_osr (alor _ isr))). by rewrite OT_prop4 //; apply: order_type_exists. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype)