Changeset 1063 for src/ASM/Vector.ma


Ignore:
Timestamp:
Jul 11, 2011, 5:52:11 PM (9 years ago)
Author:
mulligan
Message:

changes from today

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Vector.ma

    r998 r1063  
    8181    get_index_v A (S (n + m)) b n ?.
    8282  normalize
    83   //
     83  @le_S_S
     84  cases m //
    8485qed.
    8586
     
    179180  ] (? : S ? = S ?).
    180181  //
    181   [ destruct
    182   | lapply (injective_S … K)
    183     //
    184   ]
     182  lapply (injective_S … K)
     183  //
    185184qed.
    186185
     
    404403          ]
    405404    ].
    406   //
     405  /2/
    407406qed.
    408407
Note: See TracChangeset for help on using the changeset viewer.