Ignore:
Timestamp:
Nov 22, 2011, 11:58:43 AM (9 years ago)
Author:
campbell
Message:

Update most of Assembly.ma with new syntax and identifier maps.
Change positive.ma a little to reduce name clashes.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/binary/division.ma

    r1523 r1528  
    9292theorem plus_minus_r:
    9393∀m,n,p:Pos. m < n → p+(n-m) = (p+n)-m.
    94 #m #n #p #le >(commutative_plus …)
    95 >(commutative_plus p ?) @plus_minus //; qed.
     94#m #n #p #le >(commutative_plus_pos …)
     95>(commutative_plus_pos p ?) @plus_minus //; qed.
    9696
    9797lemma plus_minus_le: ∀m,n,p:Pos. m≤n → m+p-n≤p.
     
    169169  | MinusPos r ⇒ n = m+r
    170170  ].
    171 #n #m lapply (pos_compare_to_Prop n m); lapply (minus_to_plus n m);
     171#n #m lapply (pos_compare_to_Prop n m); lapply (minus_to_plus_pos n m);
    172172normalize; cases (partial_minus n m); /2/; qed.
    173173
     
    275275cases md'; [ 2,4: #md'' ] #DIVIDE  normalize;
    276276>DIV in ⊢ (% → ?); #H #lt destruct;
    277 [ lapply (plus_to_minus … e0);
     277[ lapply (plus_to_minus_pos … e0);
    278278    >(commutative_times …) >(commutative_times dv'' …)
    279279    cut (dv'' < dv); [ cut (dv''*m < dv*m); /2/; ] #dvlt
Note: See TracChangeset for help on using the changeset viewer.