+
+(* Properties with isdiv ****************************************************)
+
+corec lemma sle_isdiv_dx: ∀f2. 𝛀⦃f2⦄ → ∀f1. f1 ⊆ f2.
+#f2 * -f2
+#f2 #g2 #Hf2 #H2 #f1 cases (pn_split f1) *
+/3 width=5 by sle_weak, sle_next/
+qed.
+
+(* Inversion lemmas with isdiv **********************************************)
+
+corec lemma sle_inv_isdiv_sn: ∀f1,f2. f1 ⊆ f2 → 𝛀⦃f1⦄ → 𝛀⦃f2⦄.
+#f1 #f2 * -f1 -f2
+#f1 #f2 #g1 #g2 #Hf * * #H
+[1,3: elim (isdiv_inv_push … H) // ]
+lapply (isdiv_inv_next … H ??) -H
+/3 width=3 by isdiv_next/
+qed-.