X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fdama%2Fdama%2Fproperty_exhaustivity.ma;h=48551f85e70ab95c2867e65d4aea9b1e93fcd919;hb=f20f1ac4aea15d81599bd2283c5440fce8d4cf6a;hp=fc7121349d89c6917a7384710b211dc29a4a8e01;hpb=3f80c07b790d3abdb3aafcd1da33f14fa90ada25;p=helm.git diff --git a/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma b/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma index fc7121349..48551f85e 100644 --- a/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma +++ b/helm/software/matita/contribs/dama/dama/property_exhaustivity.ma @@ -69,22 +69,37 @@ definition exhaustive â (b is_decreasing â b is_lower_located â b is_cauchy). lemma prove_in_segment: - âO:ordered_set.âs:segment (os_l O).âx:O. - ð_s (λl.l ⤠x) â ð¦_s (λu.x ⤠u) â x â s. -intros; unfold; cases (wloss_prop (os_l O)); rewrite < H2; + âO:half_ordered_set.âs:segment O.âx:O. + seg_l O s (λl.l â¤â¤ x) â seg_u O s (λu.x â¤â¤ u) â x â s. +intros; unfold; cases (wloss_prop O); rewrite < H2; split; assumption; qed. -lemma under_wloss_upperbound: - âC:half_ordered_set.âs:segment C.âa:sequence C. - seg_u C s (upper_bound C a) â - âi.seg_u C s (λu.a i â¤â¤ u). -intros; unfold in H; unfold; -cases (wloss_prop C); rewrite