proposition: Lemma strict_lub_ref (s:nat-> hT1) (lambda: hT1) : strict_lub s lambda <-> gstrict_lub (h2g_seq s) (h2g lambda).
proof: Proof. rewrite /gstrict_lub; split. - case => Ha Hb; split. + move => i; rewrite -!LT_ref => //. + move => a Ha1; rewrite -(h2g_g2hK a) -LE_ref. apply Hb => i; destruct (Ha1 i) as [H H0 H1]; split. * move: H; rewrite -hnf_g2h /h2g_seq g2h_h2gK => //. * split. -- move: H0; rewrite T1le_iff /h2g_seq g2h_h2gK => //. -- by rewrite hnf_g2h. - destruct 1 as [H H0]; split. + move => i; move: (H i); rewrite LT_ref =>//. + move => a Ha; rewrite LE_ref; apply H0. move => i; rewrite -LE_ref; apply Ha. Qed.
imports: mathcomp(all_ssreflect zify) Coq(Logic.Eqdep_dec) hydras(DecPreOrder ON_Generic T1 E0) Coq(Relations Basics Wellfounded.Inverse_Image Wellfounded.Inclusion)